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 30832
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 2651 . . . . 5 (𝐴𝑚 (0..^𝑆)) = (𝐴𝑚 (0..^𝑆))
2 eqid 2651 . . . . 5 (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) = (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇))
3 ovexd 6720 . . . . 5 (𝜑 → (0..^𝑆) ∈ V)
4 nnex 11064 . . . . . . 7 ℕ ∈ V
54a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
6 reprpmtf1o.a . . . . . 6 (𝜑𝐴 ⊆ ℕ)
75, 6ssexd 4838 . . . . 5 (𝜑𝐴 ∈ V)
8 reprpmtf1o.x . . . . . 6 (𝜑𝑋 ∈ (0..^𝑆))
9 reprpmtf1o.s . . . . . . 7 (𝜑𝑆 ∈ ℕ)
10 lbfzo0 12547 . . . . . . 7 (0 ∈ (0..^𝑆) ↔ 𝑆 ∈ ℕ)
119, 10sylibr 224 . . . . . 6 (𝜑 → 0 ∈ (0..^𝑆))
12 reprpmtf1o.t . . . . . 6 𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0}))
133, 8, 11, 12pmtridf1o 29984 . . . . 5 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141, 1, 2, 3, 3, 7, 13fmptco1f1o 29562 . . . 4 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)))
15 f1of1 6174 . . . 4 ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)))
1614, 15syl 17 . . 3 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)))
17 ssrab2 3720 . . . . . 6 {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ⊆ (𝐴𝑚 (0..^𝑆))
18 reprpmtf1o.p . . . . . . . . . 10 𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵}
1918ssrab3 3721 . . . . . . . . 9 𝑃 ⊆ (𝐴(repr‘𝑆)𝑀)
2019a1i 11 . . . . . . . 8 (𝜑𝑃 ⊆ (𝐴(repr‘𝑆)𝑀))
21 reprpmtf1o.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
229nnnn0d 11389 . . . . . . . . 9 (𝜑𝑆 ∈ ℕ0)
236, 21, 22reprval 30816 . . . . . . . 8 (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2420, 23sseqtrd 3674 . . . . . . 7 (𝜑𝑃 ⊆ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2524sselda 3636 . . . . . 6 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2617, 25sseldi 3634 . . . . 5 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴𝑚 (0..^𝑆)))
2726ex 449 . . . 4 (𝜑 → (𝑐𝑃𝑐 ∈ (𝐴𝑚 (0..^𝑆))))
2827ssrdv 3642 . . 3 (𝜑𝑃 ⊆ (𝐴𝑚 (0..^𝑆)))
29 f1ores 6189 . . 3 (((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)) ∧ 𝑃 ⊆ (𝐴𝑚 (0..^𝑆))) → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
3016, 28, 29syl2anc 694 . 2 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
31 resmpt 5484 . . . . 5 (𝑃 ⊆ (𝐴𝑚 (0..^𝑆)) → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
3228, 31syl 17 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
33 reprpmtf1o.f . . . 4 𝐹 = (𝑐𝑃 ↦ (𝑐𝑇))
3432, 33syl6eqr 2703 . . 3 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = 𝐹)
35 eqidd 2652 . . 3 (𝜑𝑃 = 𝑃)
36 vex 3234 . . . . . . . . 9 𝑑 ∈ V
3736a1i 11 . . . . . . . 8 (𝜑𝑑 ∈ V)
382, 37, 28elimampt 29566 . . . . . . 7 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ ∃𝑐𝑃 𝑑 = (𝑐𝑇)))
39 simpr 476 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 = (𝑐𝑇))
40 f1of 6175 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4114, 40syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4241ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
432fmpt 6421 . . . . . . . . . . . . . . 15 (∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4442, 43sylibr 224 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4526adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑐 ∈ (𝐴𝑚 (0..^𝑆)))
46 rspa 2959 . . . . . . . . . . . . . 14 ((∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ∧ 𝑐 ∈ (𝐴𝑚 (0..^𝑆))) → (𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4744, 45, 46syl2anc 694 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4839, 47eqeltrd 2730 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴𝑚 (0..^𝑆)))
4939adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = (𝑐𝑇))
5049fveq1d 6231 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = ((𝑐𝑇)‘𝑎))
51 f1ofun 6177 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
5213, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝑇)
5352ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
54 simpr 476 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
55 f1odm 6179 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
5613, 55syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝑇 = (0..^𝑆))
5756ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
5854, 57eleqtrrd 2733 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
59 fvco 6313 . . . . . . . . . . . . . . . . 17 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6053, 58, 59syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6160adantlr 751 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6250, 61eqtrd 2685 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = (𝑐‘(𝑇𝑎)))
6362sumeq2dv 14477 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
64 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑏 = (𝑇𝑎) → (𝑐𝑏) = (𝑐‘(𝑇𝑎)))
65 fzofi 12813 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (0..^𝑆) ∈ Fin)
6713adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
68 eqidd 2652 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
696ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
706adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝐴 ⊆ ℕ)
7121adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑀 ∈ ℤ)
7222adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑆 ∈ ℕ0)
7320sselda 3636 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴(repr‘𝑆)𝑀))
7470, 71, 72, 73reprf 30818 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝑃) → 𝑐:(0..^𝑆)⟶𝐴)
7574ffvelrnda 6399 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ 𝐴)
7669, 75sseldd 3637 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℕ)
7776nncnd 11074 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℂ)
7864, 66, 67, 68, 77fsumf1o 14498 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
7978adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
8070, 71, 72, 73reprsum 30819 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8180adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8263, 79, 813eqtr2d 2691 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀)
83 fveq1 6228 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
8483sumeq2sdv 14479 . . . . . . . . . . . . . 14 (𝑐 = 𝑑 → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎))
8584eqeq1d 2653 . . . . . . . . . . . . 13 (𝑐 = 𝑑 → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8685elrab 3396 . . . . . . . . . . . 12 (𝑑 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ (𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8748, 82, 86sylanbrc 699 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8823ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8987, 88eleqtrrd 2733 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
9039fveq1d 6231 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑‘0) = ((𝑐𝑇)‘0))
9152ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Fun 𝑇)
9211, 56eleqtrrd 2733 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ dom 𝑇)
9392ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 0 ∈ dom 𝑇)
94 fvco 6313 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ 0 ∈ dom 𝑇) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
9591, 93, 94syl2anc 694 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
963, 8, 11, 12pmtridfv2 29986 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇‘0) = 𝑋)
9796ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑇‘0) = 𝑋)
9897fveq2d 6233 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐‘(𝑇‘0)) = (𝑐𝑋))
99 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝑃) → 𝑐𝑃)
10099, 18syl6eleq 2740 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
101 rabid 3145 . . . . . . . . . . . . . . . 16 (𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
102100, 101sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
103102simprd 478 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → ¬ (𝑐𝑋) ∈ 𝐵)
104103adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐𝑋) ∈ 𝐵)
10598, 104eqneltrd 2749 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐‘(𝑇‘0)) ∈ 𝐵)
10695, 105eqneltrd 2749 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ ((𝑐𝑇)‘0) ∈ 𝐵)
10790, 106eqneltrd 2749 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑑‘0) ∈ 𝐵)
10889, 107jca 553 . . . . . . . . 9 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
109108r19.29an 3106 . . . . . . . 8 ((𝜑 ∧ ∃𝑐𝑃 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
1106adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝐴 ⊆ ℕ)
11121adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑀 ∈ ℤ)
11222adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑆 ∈ ℕ0)
113 simpr 476 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
114110, 111, 112, 113reprf 30818 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑:(0..^𝑆)⟶𝐴)
115 f1ocnv 6187 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
116 f1of 6175 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
11713, 115, 1163syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)⟶(0..^𝑆))
118117adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
119 fco 6096 . . . . . . . . . . . . . . . . 17 ((𝑑:(0..^𝑆)⟶𝐴𝑇:(0..^𝑆)⟶(0..^𝑆)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
120114, 118, 119syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
121 elmapg 7912 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
1227, 3, 121syl2anc 694 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
123122adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
124120, 123mpbird 247 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
125124adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
126 f1ofun 6177 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
12713, 115, 1263syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → Fun 𝑇)
128127ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
129 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
130 f1odm 6179 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
13113, 115, 1303syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝑇 = (0..^𝑆))
132131adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
133129, 132eleqtrrd 2733 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
134133adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
135 fvco 6313 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
136128, 134, 135syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
137136sumeq2dv 14477 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
138 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑇𝑎) → (𝑑𝑏) = (𝑑‘(𝑇𝑎)))
13965a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (0..^𝑆) ∈ Fin)
14013, 115syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141140adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
142 eqidd 2652 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
143110adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
144114ffvelrnda 6399 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ 𝐴)
145143, 144sseldd 3637 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℕ)
146145nncnd 11074 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℂ)
147138, 139, 141, 142, 146fsumf1o 14498 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
148110, 111, 112, 113reprsum 30819 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = 𝑀)
149137, 147, 1483eqtr2d 2691 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
150149adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
151 fveq1 6228 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑑𝑇) → (𝑐𝑎) = ((𝑑𝑇)‘𝑎))
152151sumeq2sdv 14479 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑑𝑇) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎))
153152eqeq1d 2653 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
154153elrab 3396 . . . . . . . . . . . . . 14 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
155125, 150, 154sylanbrc 699 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
15623ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
157155, 156eleqtrrd 2733 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀))
158127ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Fun 𝑇)
1598, 131eleqtrrd 2733 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ dom 𝑇)
160159ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → 𝑋 ∈ dom 𝑇)
161 fvco 6313 . . . . . . . . . . . . . 14 ((Fun 𝑇𝑋 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
162158, 160, 161syl2anc 694 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
163 f1ocnvfv 6574 . . . . . . . . . . . . . . . . . 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 1365 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇𝑋) = 0)
166165ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑇𝑋) = 0)
167166fveq2d 6233 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑‘(𝑇𝑋)) = (𝑑‘0))
168 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘0) ∈ 𝐵)
169167, 168eqneltrd 2749 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘(𝑇𝑋)) ∈ 𝐵)
170162, 169eqneltrd 2749 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵)
171 fveq1 6228 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (𝑐𝑋) = ((𝑑𝑇)‘𝑋))
172171eleq1d 2715 . . . . . . . . . . . . . 14 (𝑐 = (𝑑𝑇) → ((𝑐𝑋) ∈ 𝐵 ↔ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
173172notbid 307 . . . . . . . . . . . . 13 (𝑐 = (𝑑𝑇) → (¬ (𝑐𝑋) ∈ 𝐵 ↔ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
174173elrab 3396 . . . . . . . . . . . 12 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ ((𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
175157, 170, 174sylanbrc 699 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
176175, 18syl6eleqr 2741 . . . . . . . . . 10 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ 𝑃)
177176anasss 680 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑𝑇) ∈ 𝑃)
178 simpr 476 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → 𝑐 = (𝑑𝑇))
179178coeq1d 5316 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑐𝑇) = ((𝑑𝑇) ∘ 𝑇))
180179eqeq2d 2661 . . . . . . . . 9 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑑 = (𝑐𝑇) ↔ 𝑑 = ((𝑑𝑇) ∘ 𝑇)))
181 f1ococnv1 6203 . . . . . . . . . . . . . 14 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
18213, 181syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
183182adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
184183coeq2d 5317 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ (𝑇𝑇)) = (𝑑 ∘ ( I ↾ (0..^𝑆))))
185114adantrr 753 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑:(0..^𝑆)⟶𝐴)
186 fcoi1 6116 . . . . . . . . . . . 12 (𝑑:(0..^𝑆)⟶𝐴 → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
187185, 186syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
188184, 187eqtr2d 2686 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = (𝑑 ∘ (𝑇𝑇)))
189 coass 5692 . . . . . . . . . 10 ((𝑑𝑇) ∘ 𝑇) = (𝑑 ∘ (𝑇𝑇))
190188, 189syl6eqr 2703 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = ((𝑑𝑇) ∘ 𝑇))
191177, 180, 190rspcedvd 3348 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → ∃𝑐𝑃 𝑑 = (𝑐𝑇))
192109, 191impbida 895 . . . . . . 7 (𝜑 → (∃𝑐𝑃 𝑑 = (𝑐𝑇) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
19338, 192bitrd 268 . . . . . 6 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
194 fveq1 6228 . . . . . . . . 9 (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0))
195194eleq1d 2715 . . . . . . . 8 (𝑐 = 𝑑 → ((𝑐‘0) ∈ 𝐵 ↔ (𝑑‘0) ∈ 𝐵))
196195notbid 307 . . . . . . 7 (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ 𝐵 ↔ ¬ (𝑑‘0) ∈ 𝐵))
197196elrab 3396 . . . . . 6 (𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵} ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
198193, 197syl6bbr 278 . . . . 5 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}))
199198eqrdv 2649 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵})
200 reprpmtf1o.o . . . 4 𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}
201199, 200syl6eqr 2703 . . 3 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = 𝑂)
20234, 35, 201f1oeq123d 6171 . 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 1523  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  wss 3607  ifcif 4119  {cpr 4212  cmpt 4762   I cid 5052  ccnv 5142  dom cdm 5143  cres 5145  cima 5146  ccom 5147  Fun wfun 5920  wf 5922  1-1wf1 5923  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  𝑚 cmap 7899  Fincfn 7997  0cc0 9974  cn 11058  0cn0 11330  cz 11415  ..^cfzo 12504  Σcsu 14460  pmTrspcpmtr 17907  reprcrepr 30814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-pmtr 17908  df-repr 30815
This theorem is referenced by:  hgt750lema  30863
  Copyright terms: Public domain W3C validator