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 31087
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 2765 . . . . 5 (𝐴𝑚 (0..^𝑆)) = (𝐴𝑚 (0..^𝑆))
2 eqid 2765 . . . . 5 (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) = (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇))
3 ovexd 6876 . . . . 5 (𝜑 → (0..^𝑆) ∈ V)
4 nnex 11281 . . . . . . 7 ℕ ∈ V
54a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
6 reprpmtf1o.a . . . . . 6 (𝜑𝐴 ⊆ ℕ)
75, 6ssexd 4966 . . . . 5 (𝜑𝐴 ∈ V)
8 reprpmtf1o.x . . . . . 6 (𝜑𝑋 ∈ (0..^𝑆))
9 reprpmtf1o.s . . . . . . 7 (𝜑𝑆 ∈ ℕ)
10 lbfzo0 12716 . . . . . . 7 (0 ∈ (0..^𝑆) ↔ 𝑆 ∈ ℕ)
119, 10sylibr 225 . . . . . 6 (𝜑 → 0 ∈ (0..^𝑆))
12 reprpmtf1o.t . . . . . 6 𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0}))
133, 8, 11, 12pmtridf1o 30238 . . . . 5 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141, 1, 2, 3, 3, 7, 13fmptco1f1o 29819 . . . 4 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)))
15 f1of1 6319 . . . 4 ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)))
1614, 15syl 17 . . 3 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)))
17 ssrab2 3847 . . . . . 6 {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ⊆ (𝐴𝑚 (0..^𝑆))
18 reprpmtf1o.p . . . . . . . . . 10 𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵}
1918ssrab3 3848 . . . . . . . . 9 𝑃 ⊆ (𝐴(repr‘𝑆)𝑀)
2019a1i 11 . . . . . . . 8 (𝜑𝑃 ⊆ (𝐴(repr‘𝑆)𝑀))
21 reprpmtf1o.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
229nnnn0d 11598 . . . . . . . . 9 (𝜑𝑆 ∈ ℕ0)
236, 21, 22reprval 31071 . . . . . . . 8 (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2420, 23sseqtrd 3801 . . . . . . 7 (𝜑𝑃 ⊆ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2524sselda 3761 . . . . . 6 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2617, 25sseldi 3759 . . . . 5 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴𝑚 (0..^𝑆)))
2726ex 401 . . . 4 (𝜑 → (𝑐𝑃𝑐 ∈ (𝐴𝑚 (0..^𝑆))))
2827ssrdv 3767 . . 3 (𝜑𝑃 ⊆ (𝐴𝑚 (0..^𝑆)))
29 f1ores 6334 . . 3 (((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1→(𝐴𝑚 (0..^𝑆)) ∧ 𝑃 ⊆ (𝐴𝑚 (0..^𝑆))) → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
3016, 28, 29syl2anc 579 . 2 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
31 resmpt 5626 . . . . 5 (𝑃 ⊆ (𝐴𝑚 (0..^𝑆)) → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
3228, 31syl 17 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
33 reprpmtf1o.f . . . 4 𝐹 = (𝑐𝑃 ↦ (𝑐𝑇))
3432, 33syl6eqr 2817 . . 3 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = 𝐹)
35 eqidd 2766 . . 3 (𝜑𝑃 = 𝑃)
36 vex 3353 . . . . . . . . 9 𝑑 ∈ V
3736a1i 11 . . . . . . . 8 (𝜑𝑑 ∈ V)
382, 37, 28elimampt 29823 . . . . . . 7 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ ∃𝑐𝑃 𝑑 = (𝑐𝑇)))
39 simpr 477 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 = (𝑐𝑇))
40 f1of 6320 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))–1-1-onto→(𝐴𝑚 (0..^𝑆)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4114, 40syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4241ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
432fmpt 6570 . . . . . . . . . . . . . . 15 (∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴𝑚 (0..^𝑆))⟶(𝐴𝑚 (0..^𝑆)))
4442, 43sylibr 225 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4526adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑐 ∈ (𝐴𝑚 (0..^𝑆)))
46 rspa 3077 . . . . . . . . . . . . . 14 ((∀𝑐 ∈ (𝐴𝑚 (0..^𝑆))(𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ∧ 𝑐 ∈ (𝐴𝑚 (0..^𝑆))) → (𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4744, 45, 46syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
4839, 47eqeltrd 2844 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴𝑚 (0..^𝑆)))
4939adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = (𝑐𝑇))
5049fveq1d 6377 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = ((𝑐𝑇)‘𝑎))
51 f1ofun 6322 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
5213, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝑇)
5352ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
54 simpr 477 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
55 f1odm 6324 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
5613, 55syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝑇 = (0..^𝑆))
5756ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
5854, 57eleqtrrd 2847 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
59 fvco 6463 . . . . . . . . . . . . . . . . 17 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6053, 58, 59syl2anc 579 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6160adantlr 706 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6250, 61eqtrd 2799 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = (𝑐‘(𝑇𝑎)))
6362sumeq2dv 14720 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
64 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑏 = (𝑇𝑎) → (𝑐𝑏) = (𝑐‘(𝑇𝑎)))
65 fzofi 12981 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (0..^𝑆) ∈ Fin)
6713adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
68 eqidd 2766 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
696ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
706adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝐴 ⊆ ℕ)
7121adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑀 ∈ ℤ)
7222adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑆 ∈ ℕ0)
7320sselda 3761 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴(repr‘𝑆)𝑀))
7470, 71, 72, 73reprf 31073 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝑃) → 𝑐:(0..^𝑆)⟶𝐴)
7574ffvelrnda 6549 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ 𝐴)
7669, 75sseldd 3762 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℕ)
7776nncnd 11292 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℂ)
7864, 66, 67, 68, 77fsumf1o 14741 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
7978adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
8070, 71, 72, 73reprsum 31074 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8180adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8263, 79, 813eqtr2d 2805 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀)
83 fveq1 6374 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
8483sumeq2sdv 14722 . . . . . . . . . . . . . 14 (𝑐 = 𝑑 → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎))
8584eqeq1d 2767 . . . . . . . . . . . . 13 (𝑐 = 𝑑 → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8685elrab 3519 . . . . . . . . . . . 12 (𝑑 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ (𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8748, 82, 86sylanbrc 578 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8823ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8987, 88eleqtrrd 2847 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
9039fveq1d 6377 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑‘0) = ((𝑐𝑇)‘0))
9152ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Fun 𝑇)
9211, 56eleqtrrd 2847 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ dom 𝑇)
9392ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 0 ∈ dom 𝑇)
94 fvco 6463 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ 0 ∈ dom 𝑇) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
9591, 93, 94syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
963, 8, 11, 12pmtridfv2 30240 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇‘0) = 𝑋)
9796ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑇‘0) = 𝑋)
9897fveq2d 6379 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐‘(𝑇‘0)) = (𝑐𝑋))
99 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝑃) → 𝑐𝑃)
10099, 18syl6eleq 2854 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
101 rabid 3263 . . . . . . . . . . . . . . . 16 (𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
102100, 101sylib 209 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
103102simprd 489 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → ¬ (𝑐𝑋) ∈ 𝐵)
104103adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐𝑋) ∈ 𝐵)
10598, 104eqneltrd 2863 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐‘(𝑇‘0)) ∈ 𝐵)
10695, 105eqneltrd 2863 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ ((𝑐𝑇)‘0) ∈ 𝐵)
10790, 106eqneltrd 2863 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑑‘0) ∈ 𝐵)
10889, 107jca 507 . . . . . . . . 9 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
109108r19.29an 3224 . . . . . . . 8 ((𝜑 ∧ ∃𝑐𝑃 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
1106adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝐴 ⊆ ℕ)
11121adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑀 ∈ ℤ)
11222adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑆 ∈ ℕ0)
113 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
114110, 111, 112, 113reprf 31073 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑:(0..^𝑆)⟶𝐴)
115 f1ocnv 6332 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
116 f1of 6320 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
11713, 115, 1163syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)⟶(0..^𝑆))
118117adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
119 fco 6240 . . . . . . . . . . . . . . . . 17 ((𝑑:(0..^𝑆)⟶𝐴𝑇:(0..^𝑆)⟶(0..^𝑆)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
120114, 118, 119syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
121 elmapg 8073 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
1227, 3, 121syl2anc 579 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
123122adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
124120, 123mpbird 248 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
125124adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)))
126 f1ofun 6322 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
12713, 115, 1263syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → Fun 𝑇)
128127ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
129 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
130 f1odm 6324 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
13113, 115, 1303syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝑇 = (0..^𝑆))
132131adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
133129, 132eleqtrrd 2847 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
134133adantlr 706 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
135 fvco 6463 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
136128, 134, 135syl2anc 579 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
137136sumeq2dv 14720 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
138 fveq2 6375 . . . . . . . . . . . . . . . . 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 2766 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
143110adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
144114ffvelrnda 6549 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ 𝐴)
145143, 144sseldd 3762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℕ)
146145nncnd 11292 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℂ)
147138, 139, 141, 142, 146fsumf1o 14741 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
148110, 111, 112, 113reprsum 31074 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = 𝑀)
149137, 147, 1483eqtr2d 2805 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
150149adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
151 fveq1 6374 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑑𝑇) → (𝑐𝑎) = ((𝑑𝑇)‘𝑎))
152151sumeq2sdv 14722 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑑𝑇) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎))
153152eqeq1d 2767 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
154153elrab 3519 . . . . . . . . . . . . . 14 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ ((𝑑𝑇) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
155125, 150, 154sylanbrc 578 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
15623ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
157155, 156eleqtrrd 2847 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀))
158127ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Fun 𝑇)
1598, 131eleqtrrd 2847 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ dom 𝑇)
160159ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → 𝑋 ∈ dom 𝑇)
161 fvco 6463 . . . . . . . . . . . . . 14 ((Fun 𝑇𝑋 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
162158, 160, 161syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
163 f1ocnvfv 6726 . . . . . . . . . . . . . . . . . 18 ((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) → ((𝑇‘0) = 𝑋 → (𝑇𝑋) = 0))
164163imp 395 . . . . . . . . . . . . . . . . 17 (((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) ∧ (𝑇‘0) = 𝑋) → (𝑇𝑋) = 0)
16513, 11, 96, 164syl21anc 866 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇𝑋) = 0)
166165ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑇𝑋) = 0)
167166fveq2d 6379 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑‘(𝑇𝑋)) = (𝑑‘0))
168 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘0) ∈ 𝐵)
169167, 168eqneltrd 2863 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘(𝑇𝑋)) ∈ 𝐵)
170162, 169eqneltrd 2863 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵)
171 fveq1 6374 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (𝑐𝑋) = ((𝑑𝑇)‘𝑋))
172171eleq1d 2829 . . . . . . . . . . . . . 14 (𝑐 = (𝑑𝑇) → ((𝑐𝑋) ∈ 𝐵 ↔ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
173172notbid 309 . . . . . . . . . . . . 13 (𝑐 = (𝑑𝑇) → (¬ (𝑐𝑋) ∈ 𝐵 ↔ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
174173elrab 3519 . . . . . . . . . . . 12 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ ((𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
175157, 170, 174sylanbrc 578 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
176175, 18syl6eleqr 2855 . . . . . . . . . 10 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ 𝑃)
177176anasss 458 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑𝑇) ∈ 𝑃)
178 simpr 477 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → 𝑐 = (𝑑𝑇))
179178coeq1d 5452 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑐𝑇) = ((𝑑𝑇) ∘ 𝑇))
180179eqeq2d 2775 . . . . . . . . 9 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑑 = (𝑐𝑇) ↔ 𝑑 = ((𝑑𝑇) ∘ 𝑇)))
181 f1ococnv1 6348 . . . . . . . . . . . . . 14 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
18213, 181syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
183182adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
184183coeq2d 5453 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ (𝑇𝑇)) = (𝑑 ∘ ( I ↾ (0..^𝑆))))
185114adantrr 708 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑:(0..^𝑆)⟶𝐴)
186 fcoi1 6260 . . . . . . . . . . . 12 (𝑑:(0..^𝑆)⟶𝐴 → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
187185, 186syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
188184, 187eqtr2d 2800 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = (𝑑 ∘ (𝑇𝑇)))
189 coass 5840 . . . . . . . . . 10 ((𝑑𝑇) ∘ 𝑇) = (𝑑 ∘ (𝑇𝑇))
190188, 189syl6eqr 2817 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = ((𝑑𝑇) ∘ 𝑇))
191177, 180, 190rspcedvd 3468 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → ∃𝑐𝑃 𝑑 = (𝑐𝑇))
192109, 191impbida 835 . . . . . . 7 (𝜑 → (∃𝑐𝑃 𝑑 = (𝑐𝑇) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
19338, 192bitrd 270 . . . . . 6 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
194 fveq1 6374 . . . . . . . . 9 (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0))
195194eleq1d 2829 . . . . . . . 8 (𝑐 = 𝑑 → ((𝑐‘0) ∈ 𝐵 ↔ (𝑑‘0) ∈ 𝐵))
196195notbid 309 . . . . . . 7 (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ 𝐵 ↔ ¬ (𝑑‘0) ∈ 𝐵))
197196elrab 3519 . . . . . 6 (𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵} ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
198193, 197syl6bbr 280 . . . . 5 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}))
199198eqrdv 2763 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵})
200 reprpmtf1o.o . . . 4 𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}
201199, 200syl6eqr 2817 . . 3 (𝜑 → ((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = 𝑂)
20234, 35, 201f1oeq123d 6316 . 2 (𝜑 → (((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴𝑚 (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝐹:𝑃1-1-onto𝑂))
20330, 202mpbid 223 1 (𝜑𝐹:𝑃1-1-onto𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  wss 3732  ifcif 4243  {cpr 4336  cmpt 4888   I cid 5184  ccnv 5276  dom cdm 5277  cres 5279  cima 5280  ccom 5281  Fun wfun 6062  wf 6064  1-1wf1 6065  1-1-ontowf1o 6067  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  Fincfn 8160  0cc0 10189  cn 11274  0cn0 11538  cz 11624  ..^cfzo 12673  Σcsu 14703  pmTrspcpmtr 18126  reprcrepr 31069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-sum 14704  df-pmtr 18127  df-repr 31070
This theorem is referenced by:  hgt750lema  31118
  Copyright terms: Public domain W3C validator