Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  reprpmtf1o Structured version   Visualization version   GIF version

Theorem reprpmtf1o 31011
Description: Transposing 0 and 𝑋 maps representations with a condition on the first index to transpositions with the same condition on the index 𝑋. (Contributed by Thierry Arnoux, 27-Dec-2021.)
Hypotheses
Ref Expression
reprpmtf1o.s (𝜑𝑆 ∈ ℕ)
reprpmtf1o.m (𝜑𝑀 ∈ ℤ)
reprpmtf1o.a (𝜑𝐴 ⊆ ℕ)
reprpmtf1o.x (𝜑𝑋 ∈ (0..^𝑆))
reprpmtf1o.o 𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}
reprpmtf1o.p 𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵}
reprpmtf1o.t 𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0}))
reprpmtf1o.f 𝐹 = (𝑐𝑃 ↦ (𝑐𝑇))
Assertion
Ref Expression
reprpmtf1o (𝜑𝐹:𝑃1-1-onto𝑂)
Distinct variable groups:   𝐴,𝑐   𝐵,𝑐   𝑀,𝑐   𝑃,𝑐   𝑆,𝑐   𝑇,𝑐   𝑋,𝑐   𝜑,𝑐
Allowed substitution hints:   𝐹(𝑐)   𝑂(𝑐)

Proof of Theorem reprpmtf1o
Dummy variables 𝑎 𝑏 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2758 . . . . 5 (𝐴𝑚 (0..^𝑆)) = (𝐴𝑚 (0..^𝑆))
2 eqid 2758 . . . . 5 (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) = (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇))
3 ovexd 6841 . . . . 5 (𝜑 → (0..^𝑆) ∈ V)
4 nnex 11216 . . . . . . 7 ℕ ∈ V
54a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
6 reprpmtf1o.a . . . . . 6 (𝜑𝐴 ⊆ ℕ)
75, 6ssexd 4955 . . . . 5 (𝜑𝐴 ∈ V)
8 reprpmtf1o.x . . . . . 6 (𝜑𝑋 ∈ (0..^𝑆))
9 reprpmtf1o.s . . . . . . 7 (𝜑𝑆 ∈ ℕ)
10 lbfzo0 12700 . . . . . . 7 (0 ∈ (0..^𝑆) ↔ 𝑆 ∈ ℕ)
119, 10sylibr 224 . . . . . 6 (𝜑 → 0 ∈ (0..^𝑆))
12 reprpmtf1o.t . . . . . 6 𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0}))
133, 8, 11, 12pmtridf1o 30163 . . . . 5 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141, 1, 2, 3, 3, 7, 13fmptco1f1o 29741 . . . 4 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)))
15 f1of1 6295 . . . 4 ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)))
1614, 15syl 17 . . 3 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)))
17 ssrab2 3826 . . . . . 6 {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ⊆ (𝐴𝑚 (0..^𝑆))
18 reprpmtf1o.p . . . . . . . . . 10 𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵}
1918ssrab3 3827 . . . . . . . . 9 𝑃 ⊆ (𝐴(repr‘𝑆)𝑀)
2019a1i 11 . . . . . . . 8 (𝜑𝑃 ⊆ (𝐴(repr‘𝑆)𝑀))
21 reprpmtf1o.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
229nnnn0d 11541 . . . . . . . . 9 (𝜑𝑆 ∈ ℕ0)
236, 21, 22reprval 30995 . . . . . . . 8 (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2420, 23sseqtrd 3780 . . . . . . 7 (𝜑𝑃 ⊆ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2524sselda 3742 . . . . . 6 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2617, 25sseldi 3740 . . . . 5 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴𝑚 (0..^𝑆)))
2726ex 449 . . . 4 (𝜑 → (𝑐𝑃𝑐 ∈ (𝐴𝑚 (0..^𝑆))))
2827ssrdv 3748 . . 3 (𝜑𝑃 ⊆ (𝐴𝑚 (0..^𝑆)))
29 f1ores 6310 . . 3 (((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)) ∧ 𝑃 ⊆ (𝐴𝑚 (0..^𝑆))) → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
3016, 28, 29syl2anc 696 . 2 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
31 resmpt 5605 . . . . 5 (𝑃 ⊆ (𝐴𝑚 (0..^𝑆)) → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
3228, 31syl 17 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
33 reprpmtf1o.f . . . 4 𝐹 = (𝑐𝑃 ↦ (𝑐𝑇))
3432, 33syl6eqr 2810 . . 3 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = 𝐹)
35 eqidd 2759 . . 3 (𝜑𝑃 = 𝑃)
36 vex 3341 . . . . . . . . 9 𝑑 ∈ V
3736a1i 11 . . . . . . . 8 (𝜑𝑑 ∈ V)
382, 37, 28elimampt 29745 . . . . . . 7 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ ∃𝑐𝑃 𝑑 = (𝑐𝑇)))
39 simpr 479 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 = (𝑐𝑇))
40 f1of 6296 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4114, 40syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4241ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
432fmpt 6542 . . . . . . . . . . . . . . 15 (∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4442, 43sylibr 224 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4526adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑐 ∈ (𝐴𝑚 (0..^𝑆)))
46 rspa 3066 . . . . . . . . . . . . . 14 ((∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ∧ 𝑐 ∈ (𝐴𝑚 (0..^𝑆))) → (𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4744, 45, 46syl2anc 696 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4839, 47eqeltrd 2837 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴𝑚 (0..^𝑆)))
4939adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = (𝑐𝑇))
5049fveq1d 6352 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = ((𝑐𝑇)‘𝑎))
51 f1ofun 6298 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
5213, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝑇)
5352ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
54 simpr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
55 f1odm 6300 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
5613, 55syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝑇 = (0..^𝑆))
5756ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
5854, 57eleqtrrd 2840 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
59 fvco 6434 . . . . . . . . . . . . . . . . 17 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6053, 58, 59syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6160adantlr 753 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6250, 61eqtrd 2792 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = (𝑐‘(𝑇𝑎)))
6362sumeq2dv 14630 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
64 fveq2 6350 . . . . . . . . . . . . . . 15 (𝑏 = (𝑇𝑎) → (𝑐𝑏) = (𝑐‘(𝑇𝑎)))
65 fzofi 12965 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (0..^𝑆) ∈ Fin)
6713adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
68 eqidd 2759 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
696ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
706adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝐴 ⊆ ℕ)
7121adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑀 ∈ ℤ)
7222adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑆 ∈ ℕ0)
7320sselda 3742 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴(repr‘𝑆)𝑀))
7470, 71, 72, 73reprf 30997 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝑃) → 𝑐:(0..^𝑆)⟶𝐴)
7574ffvelrnda 6520 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ 𝐴)
7669, 75sseldd 3743 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℕ)
7776nncnd 11226 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℂ)
7864, 66, 67, 68, 77fsumf1o 14651 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
7978adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
8070, 71, 72, 73reprsum 30998 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8180adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8263, 79, 813eqtr2d 2798 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀)
83 fveq1 6349 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
8483sumeq2sdv 14632 . . . . . . . . . . . . . 14 (𝑐 = 𝑑 → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎))
8584eqeq1d 2760 . . . . . . . . . . . . 13 (𝑐 = 𝑑 → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8685elrab 3502 . . . . . . . . . . . 12 (𝑑 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ (𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8748, 82, 86sylanbrc 701 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8823ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8987, 88eleqtrrd 2840 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
9039fveq1d 6352 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑‘0) = ((𝑐𝑇)‘0))
9152ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Fun 𝑇)
9211, 56eleqtrrd 2840 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ dom 𝑇)
9392ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 0 ∈ dom 𝑇)
94 fvco 6434 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ 0 ∈ dom 𝑇) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
9591, 93, 94syl2anc 696 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
963, 8, 11, 12pmtridfv2 30165 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇‘0) = 𝑋)
9796ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑇‘0) = 𝑋)
9897fveq2d 6354 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐‘(𝑇‘0)) = (𝑐𝑋))
99 simpr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝑃) → 𝑐𝑃)
10099, 18syl6eleq 2847 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
101 rabid 3252 . . . . . . . . . . . . . . . 16 (𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
102100, 101sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
103102simprd 482 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → ¬ (𝑐𝑋) ∈ 𝐵)
104103adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐𝑋) ∈ 𝐵)
10598, 104eqneltrd 2856 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐‘(𝑇‘0)) ∈ 𝐵)
10695, 105eqneltrd 2856 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ ((𝑐𝑇)‘0) ∈ 𝐵)
10790, 106eqneltrd 2856 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑑‘0) ∈ 𝐵)
10889, 107jca 555 . . . . . . . . 9 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
109108r19.29an 3213 . . . . . . . 8 ((𝜑 ∧ ∃𝑐𝑃 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
1106adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝐴 ⊆ ℕ)
11121adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑀 ∈ ℤ)
11222adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑆 ∈ ℕ0)
113 simpr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
114110, 111, 112, 113reprf 30997 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑:(0..^𝑆)⟶𝐴)
115 f1ocnv 6308 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
116 f1of 6296 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
11713, 115, 1163syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)⟶(0..^𝑆))
118117adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
119 fco 6217 . . . . . . . . . . . . . . . . 17 ((𝑑:(0..^𝑆)⟶𝐴𝑇:(0..^𝑆)⟶(0..^𝑆)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
120114, 118, 119syl2anc 696 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
121 elmapg 8034 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
1227, 3, 121syl2anc 696 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
123122adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
124120, 123mpbird 247 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
125124adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
126 f1ofun 6298 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
12713, 115, 1263syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → Fun 𝑇)
128127ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
129 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
130 f1odm 6300 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
13113, 115, 1303syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝑇 = (0..^𝑆))
132131adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
133129, 132eleqtrrd 2840 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
134133adantlr 753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
135 fvco 6434 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
136128, 134, 135syl2anc 696 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
137136sumeq2dv 14630 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
138 fveq2 6350 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑇𝑎) → (𝑑𝑏) = (𝑑‘(𝑇𝑎)))
13965a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (0..^𝑆) ∈ Fin)
14013, 115syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141140adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
142 eqidd 2759 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
143110adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
144114ffvelrnda 6520 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ 𝐴)
145143, 144sseldd 3743 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℕ)
146145nncnd 11226 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℂ)
147138, 139, 141, 142, 146fsumf1o 14651 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
148110, 111, 112, 113reprsum 30998 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = 𝑀)
149137, 147, 1483eqtr2d 2798 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
150149adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
151 fveq1 6349 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑑𝑇) → (𝑐𝑎) = ((𝑑𝑇)‘𝑎))
152151sumeq2sdv 14632 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑑𝑇) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎))
153152eqeq1d 2760 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
154153elrab 3502 . . . . . . . . . . . . . 14 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
155125, 150, 154sylanbrc 701 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
15623ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
157155, 156eleqtrrd 2840 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀))
158127ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Fun 𝑇)
1598, 131eleqtrrd 2840 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ dom 𝑇)
160159ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → 𝑋 ∈ dom 𝑇)
161 fvco 6434 . . . . . . . . . . . . . 14 ((Fun 𝑇𝑋 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
162158, 160, 161syl2anc 696 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
163 f1ocnvfv 6695 . . . . . . . . . . . . . . . . . 18 ((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) → ((𝑇‘0) = 𝑋 → (𝑇𝑋) = 0))
164163imp 444 . . . . . . . . . . . . . . . . 17 (((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) ∧ (𝑇‘0) = 𝑋) → (𝑇𝑋) = 0)
16513, 11, 96, 164syl21anc 1476 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇𝑋) = 0)
166165ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑇𝑋) = 0)
167166fveq2d 6354 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑‘(𝑇𝑋)) = (𝑑‘0))
168 simpr 479 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘0) ∈ 𝐵)
169167, 168eqneltrd 2856 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘(𝑇𝑋)) ∈ 𝐵)
170162, 169eqneltrd 2856 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵)
171 fveq1 6349 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (𝑐𝑋) = ((𝑑𝑇)‘𝑋))
172171eleq1d 2822 . . . . . . . . . . . . . 14 (𝑐 = (𝑑𝑇) → ((𝑐𝑋) ∈ 𝐵 ↔ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
173172notbid 307 . . . . . . . . . . . . 13 (𝑐 = (𝑑𝑇) → (¬ (𝑐𝑋) ∈ 𝐵 ↔ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
174173elrab 3502 . . . . . . . . . . . 12 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ ((𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
175157, 170, 174sylanbrc 701 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
176175, 18syl6eleqr 2848 . . . . . . . . . 10 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ 𝑃)
177176anasss 682 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑𝑇) ∈ 𝑃)
178 simpr 479 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → 𝑐 = (𝑑𝑇))
179178coeq1d 5437 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑐𝑇) = ((𝑑𝑇) ∘ 𝑇))
180179eqeq2d 2768 . . . . . . . . 9 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑑 = (𝑐𝑇) ↔ 𝑑 = ((𝑑𝑇) ∘ 𝑇)))
181 f1ococnv1 6324 . . . . . . . . . . . . . 14 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
18213, 181syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
183182adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
184183coeq2d 5438 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ (𝑇𝑇)) = (𝑑 ∘ ( I ↾ (0..^𝑆))))
185114adantrr 755 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑:(0..^𝑆)⟶𝐴)
186 fcoi1 6237 . . . . . . . . . . . 12 (𝑑:(0..^𝑆)⟶𝐴 → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
187185, 186syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
188184, 187eqtr2d 2793 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = (𝑑 ∘ (𝑇𝑇)))
189 coass 5813 . . . . . . . . . 10 ((𝑑𝑇) ∘ 𝑇) = (𝑑 ∘ (𝑇𝑇))
190188, 189syl6eqr 2810 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = ((𝑑𝑇) ∘ 𝑇))
191177, 180, 190rspcedvd 3454 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → ∃𝑐𝑃 𝑑 = (𝑐𝑇))
192109, 191impbida 913 . . . . . . 7 (𝜑 → (∃𝑐𝑃 𝑑 = (𝑐𝑇) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
19338, 192bitrd 268 . . . . . 6 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
194 fveq1 6349 . . . . . . . . 9 (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0))
195194eleq1d 2822 . . . . . . . 8 (𝑐 = 𝑑 → ((𝑐‘0) ∈ 𝐵 ↔ (𝑑‘0) ∈ 𝐵))
196195notbid 307 . . . . . . 7 (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ 𝐵 ↔ ¬ (𝑑‘0) ∈ 𝐵))
197196elrab 3502 . . . . . 6 (𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵} ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
198193, 197syl6bbr 278 . . . . 5 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}))
199198eqrdv 2756 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵})
200 reprpmtf1o.o . . . 4 𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}
201199, 200syl6eqr 2810 . . 3 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = 𝑂)
20234, 35, 201f1oeq123d 6292 . 2 (𝜑 → (((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝐹:𝑃1-1-onto𝑂))
20330, 202mpbid 222 1 (𝜑𝐹:𝑃1-1-onto𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1630  wcel 2137  wral 3048  wrex 3049  {crab 3052  Vcvv 3338  wss 3713  ifcif 4228  {cpr 4321  cmpt 4879   I cid 5171  ccnv 5263  dom cdm 5264  cres 5266  cima 5267  ccom 5268  Fun wfun 6041  wf 6043  1-1wf1 6044  1-1-ontowf1o 6046  cfv 6047  (class class class)co 6811  𝑚 cmap 8021  Fincfn 8119  0cc0 10126  cn 11210  0cn0 11482  cz 11567  ..^cfzo 12657  Σcsu 14613  pmTrspcpmtr 18059  reprcrepr 30993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-inf2 8709  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-map 8023  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-sup 8511  df-oi 8578  df-card 8953  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-n0 11483  df-z 11568  df-uz 11878  df-rp 12024  df-fz 12518  df-fzo 12658  df-seq 12994  df-exp 13053  df-hash 13310  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-clim 14416  df-sum 14614  df-pmtr 18060  df-repr 30994
This theorem is referenced by:  hgt750lema  31042
  Copyright terms: Public domain W3C validator