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 34619
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 2734 . . . . 5 (𝐴m (0..^𝑆)) = (𝐴m (0..^𝑆))
2 eqid 2734 . . . . 5 (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) = (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇))
3 ovexd 7465 . . . . 5 (𝜑 → (0..^𝑆) ∈ V)
4 nnex 12269 . . . . . . 7 ℕ ∈ V
54a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
6 reprpmtf1o.a . . . . . 6 (𝜑𝐴 ⊆ ℕ)
75, 6ssexd 5329 . . . . 5 (𝜑𝐴 ∈ V)
8 reprpmtf1o.x . . . . . 6 (𝜑𝑋 ∈ (0..^𝑆))
9 reprpmtf1o.s . . . . . . 7 (𝜑𝑆 ∈ ℕ)
10 lbfzo0 13735 . . . . . . 7 (0 ∈ (0..^𝑆) ↔ 𝑆 ∈ ℕ)
119, 10sylibr 234 . . . . . 6 (𝜑 → 0 ∈ (0..^𝑆))
12 reprpmtf1o.t . . . . . 6 𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0}))
133, 8, 11, 12pmtridf1o 33096 . . . . 5 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141, 1, 2, 3, 3, 7, 13fmptco1f1o 32649 . . . 4 (𝜑 → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1-onto→(𝐴m (0..^𝑆)))
15 f1of1 6847 . . . 4 ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1-onto→(𝐴m (0..^𝑆)) → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1→(𝐴m (0..^𝑆)))
1614, 15syl 17 . . 3 (𝜑 → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1→(𝐴m (0..^𝑆)))
17 ssrab2 4089 . . . . . 6 {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ⊆ (𝐴m (0..^𝑆))
18 reprpmtf1o.p . . . . . . . . . 10 𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵}
1918ssrab3 4091 . . . . . . . . 9 𝑃 ⊆ (𝐴(repr‘𝑆)𝑀)
2019a1i 11 . . . . . . . 8 (𝜑𝑃 ⊆ (𝐴(repr‘𝑆)𝑀))
21 reprpmtf1o.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
229nnnn0d 12584 . . . . . . . . 9 (𝜑𝑆 ∈ ℕ0)
236, 21, 22reprval 34603 . . . . . . . 8 (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2420, 23sseqtrd 4035 . . . . . . 7 (𝜑𝑃 ⊆ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2524sselda 3994 . . . . . 6 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2617, 25sselid 3992 . . . . 5 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴m (0..^𝑆)))
2726ex 412 . . . 4 (𝜑 → (𝑐𝑃𝑐 ∈ (𝐴m (0..^𝑆))))
2827ssrdv 4000 . . 3 (𝜑𝑃 ⊆ (𝐴m (0..^𝑆)))
29 f1ores 6862 . . 3 (((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1→(𝐴m (0..^𝑆)) ∧ 𝑃 ⊆ (𝐴m (0..^𝑆))) → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
3016, 28, 29syl2anc 584 . 2 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
31 resmpt 6056 . . . . 5 (𝑃 ⊆ (𝐴m (0..^𝑆)) → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
3228, 31syl 17 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
33 reprpmtf1o.f . . . 4 𝐹 = (𝑐𝑃 ↦ (𝑐𝑇))
3432, 33eqtr4di 2792 . . 3 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = 𝐹)
35 eqidd 2735 . . 3 (𝜑𝑃 = 𝑃)
36 vex 3481 . . . . . . . . 9 𝑑 ∈ V
3736a1i 11 . . . . . . . 8 (𝜑𝑑 ∈ V)
382, 37, 28elimampt 6062 . . . . . . 7 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ ∃𝑐𝑃 𝑑 = (𝑐𝑇)))
39 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 = (𝑐𝑇))
40 f1of 6848 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1-onto→(𝐴m (0..^𝑆)) → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))⟶(𝐴m (0..^𝑆)))
4114, 40syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))⟶(𝐴m (0..^𝑆)))
4241ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))⟶(𝐴m (0..^𝑆)))
432fmpt 7129 . . . . . . . . . . . . . . 15 (∀𝑐 ∈ (𝐴m (0..^𝑆))(𝑐𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))⟶(𝐴m (0..^𝑆)))
4442, 43sylibr 234 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ∀𝑐 ∈ (𝐴m (0..^𝑆))(𝑐𝑇) ∈ (𝐴m (0..^𝑆)))
4526adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑐 ∈ (𝐴m (0..^𝑆)))
46 rspa 3245 . . . . . . . . . . . . . 14 ((∀𝑐 ∈ (𝐴m (0..^𝑆))(𝑐𝑇) ∈ (𝐴m (0..^𝑆)) ∧ 𝑐 ∈ (𝐴m (0..^𝑆))) → (𝑐𝑇) ∈ (𝐴m (0..^𝑆)))
4744, 45, 46syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐𝑇) ∈ (𝐴m (0..^𝑆)))
4839, 47eqeltrd 2838 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴m (0..^𝑆)))
4939adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = (𝑐𝑇))
5049fveq1d 6908 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = ((𝑐𝑇)‘𝑎))
51 f1ofun 6850 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
5213, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝑇)
5352ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
54 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
55 f1odm 6852 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
5613, 55syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝑇 = (0..^𝑆))
5756ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
5854, 57eleqtrrd 2841 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
59 fvco 7006 . . . . . . . . . . . . . . . . 17 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6053, 58, 59syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6160adantlr 715 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6250, 61eqtrd 2774 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = (𝑐‘(𝑇𝑎)))
6362sumeq2dv 15734 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
64 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑏 = (𝑇𝑎) → (𝑐𝑏) = (𝑐‘(𝑇𝑎)))
65 fzofi 14011 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (0..^𝑆) ∈ Fin)
6713adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
68 eqidd 2735 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
696ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
706adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝐴 ⊆ ℕ)
7121adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑀 ∈ ℤ)
7222adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑆 ∈ ℕ0)
7320sselda 3994 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴(repr‘𝑆)𝑀))
7470, 71, 72, 73reprf 34605 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝑃) → 𝑐:(0..^𝑆)⟶𝐴)
7574ffvelcdmda 7103 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ 𝐴)
7669, 75sseldd 3995 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℕ)
7776nncnd 12279 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℂ)
7864, 66, 67, 68, 77fsumf1o 15755 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
7978adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
8070, 71, 72, 73reprsum 34606 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8180adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8263, 79, 813eqtr2d 2780 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀)
83 fveq1 6905 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
8483sumeq2sdv 15735 . . . . . . . . . . . . . 14 (𝑐 = 𝑑 → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎))
8584eqeq1d 2736 . . . . . . . . . . . . 13 (𝑐 = 𝑑 → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8685elrab 3694 . . . . . . . . . . . 12 (𝑑 ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ (𝑑 ∈ (𝐴m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8748, 82, 86sylanbrc 583 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8823ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8987, 88eleqtrrd 2841 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
9039fveq1d 6908 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑‘0) = ((𝑐𝑇)‘0))
9152ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Fun 𝑇)
9211, 56eleqtrrd 2841 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ dom 𝑇)
9392ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 0 ∈ dom 𝑇)
94 fvco 7006 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ 0 ∈ dom 𝑇) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
9591, 93, 94syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
963, 8, 11, 12pmtridfv2 33098 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇‘0) = 𝑋)
9796ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑇‘0) = 𝑋)
9897fveq2d 6910 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐‘(𝑇‘0)) = (𝑐𝑋))
99 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝑃) → 𝑐𝑃)
10099, 18eleqtrdi 2848 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
101 rabid 3454 . . . . . . . . . . . . . . . 16 (𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
102100, 101sylib 218 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
103102simprd 495 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → ¬ (𝑐𝑋) ∈ 𝐵)
104103adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐𝑋) ∈ 𝐵)
10598, 104eqneltrd 2858 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐‘(𝑇‘0)) ∈ 𝐵)
10695, 105eqneltrd 2858 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ ((𝑐𝑇)‘0) ∈ 𝐵)
10790, 106eqneltrd 2858 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑑‘0) ∈ 𝐵)
10889, 107jca 511 . . . . . . . . 9 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
109108r19.29an 3155 . . . . . . . 8 ((𝜑 ∧ ∃𝑐𝑃 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
1106adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝐴 ⊆ ℕ)
11121adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑀 ∈ ℤ)
11222adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑆 ∈ ℕ0)
113 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
114110, 111, 112, 113reprf 34605 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑:(0..^𝑆)⟶𝐴)
115 f1ocnv 6860 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
116 f1of 6848 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
11713, 115, 1163syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)⟶(0..^𝑆))
118117adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
119 fco 6760 . . . . . . . . . . . . . . . . 17 ((𝑑:(0..^𝑆)⟶𝐴𝑇:(0..^𝑆)⟶(0..^𝑆)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
120114, 118, 119syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
121 elmapg 8877 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
1227, 3, 121syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
123122adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
124120, 123mpbird 257 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇) ∈ (𝐴m (0..^𝑆)))
125124adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴m (0..^𝑆)))
126 f1ofun 6850 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
12713, 115, 1263syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → Fun 𝑇)
128127ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
129 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
130 f1odm 6852 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
13113, 115, 1303syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝑇 = (0..^𝑆))
132131adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
133129, 132eleqtrrd 2841 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
134133adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
135 fvco 7006 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
136128, 134, 135syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
137136sumeq2dv 15734 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
138 fveq2 6906 . . . . . . . . . . . . . . . . 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 2735 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
143110adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
144114ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ 𝐴)
145143, 144sseldd 3995 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℕ)
146145nncnd 12279 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℂ)
147138, 139, 141, 142, 146fsumf1o 15755 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
148110, 111, 112, 113reprsum 34606 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = 𝑀)
149137, 147, 1483eqtr2d 2780 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
150149adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
151 fveq1 6905 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑑𝑇) → (𝑐𝑎) = ((𝑑𝑇)‘𝑎))
152151sumeq2sdv 15735 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑑𝑇) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎))
153152eqeq1d 2736 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
154153elrab 3694 . . . . . . . . . . . . . 14 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
155125, 150, 154sylanbrc 583 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
15623ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
157155, 156eleqtrrd 2841 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀))
158127ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Fun 𝑇)
1598, 131eleqtrrd 2841 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ dom 𝑇)
160159ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → 𝑋 ∈ dom 𝑇)
161 fvco 7006 . . . . . . . . . . . . . 14 ((Fun 𝑇𝑋 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
162158, 160, 161syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
163 f1ocnvfv 7297 . . . . . . . . . . . . . . . . . 18 ((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) → ((𝑇‘0) = 𝑋 → (𝑇𝑋) = 0))
164163imp 406 . . . . . . . . . . . . . . . . 17 (((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) ∧ (𝑇‘0) = 𝑋) → (𝑇𝑋) = 0)
16513, 11, 96, 164syl21anc 838 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇𝑋) = 0)
166165ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑇𝑋) = 0)
167166fveq2d 6910 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑‘(𝑇𝑋)) = (𝑑‘0))
168 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘0) ∈ 𝐵)
169167, 168eqneltrd 2858 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘(𝑇𝑋)) ∈ 𝐵)
170162, 169eqneltrd 2858 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵)
171 fveq1 6905 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (𝑐𝑋) = ((𝑑𝑇)‘𝑋))
172171eleq1d 2823 . . . . . . . . . . . . . 14 (𝑐 = (𝑑𝑇) → ((𝑐𝑋) ∈ 𝐵 ↔ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
173172notbid 318 . . . . . . . . . . . . 13 (𝑐 = (𝑑𝑇) → (¬ (𝑐𝑋) ∈ 𝐵 ↔ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
174173elrab 3694 . . . . . . . . . . . 12 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ ((𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
175157, 170, 174sylanbrc 583 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
176175, 18eleqtrrdi 2849 . . . . . . . . . 10 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ 𝑃)
177176anasss 466 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑𝑇) ∈ 𝑃)
178 simpr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → 𝑐 = (𝑑𝑇))
179178coeq1d 5874 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑐𝑇) = ((𝑑𝑇) ∘ 𝑇))
180179eqeq2d 2745 . . . . . . . . 9 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑑 = (𝑐𝑇) ↔ 𝑑 = ((𝑑𝑇) ∘ 𝑇)))
181 f1ococnv1 6877 . . . . . . . . . . . . . 14 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
18213, 181syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
183182adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
184183coeq2d 5875 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ (𝑇𝑇)) = (𝑑 ∘ ( I ↾ (0..^𝑆))))
185114adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑:(0..^𝑆)⟶𝐴)
186 fcoi1 6782 . . . . . . . . . . . 12 (𝑑:(0..^𝑆)⟶𝐴 → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
187185, 186syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
188184, 187eqtr2d 2775 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = (𝑑 ∘ (𝑇𝑇)))
189 coass 6286 . . . . . . . . . 10 ((𝑑𝑇) ∘ 𝑇) = (𝑑 ∘ (𝑇𝑇))
190188, 189eqtr4di 2792 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = ((𝑑𝑇) ∘ 𝑇))
191177, 180, 190rspcedvd 3623 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → ∃𝑐𝑃 𝑑 = (𝑐𝑇))
192109, 191impbida 801 . . . . . . 7 (𝜑 → (∃𝑐𝑃 𝑑 = (𝑐𝑇) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
19338, 192bitrd 279 . . . . . 6 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
194 fveq1 6905 . . . . . . . . 9 (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0))
195194eleq1d 2823 . . . . . . . 8 (𝑐 = 𝑑 → ((𝑐‘0) ∈ 𝐵 ↔ (𝑑‘0) ∈ 𝐵))
196195notbid 318 . . . . . . 7 (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ 𝐵 ↔ ¬ (𝑑‘0) ∈ 𝐵))
197196elrab 3694 . . . . . 6 (𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵} ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
198193, 197bitr4di 289 . . . . 5 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}))
199198eqrdv 2732 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵})
200 reprpmtf1o.o . . . 4 𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}
201199, 200eqtr4di 2792 . . 3 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = 𝑂)
20234, 35, 201f1oeq123d 6842 . 2 (𝜑 → (((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝐹:𝑃1-1-onto𝑂))
20330, 202mpbid 232 1 (𝜑𝐹:𝑃1-1-onto𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  wss 3962  ifcif 4530  {cpr 4632  cmpt 5230   I cid 5581  ccnv 5687  dom cdm 5688  cres 5690  cima 5691  ccom 5692  Fun wfun 6556  wf 6558  1-1wf1 6559  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  m cmap 8864  Fincfn 8983  0cc0 11152  cn 12263  0cn0 12523  cz 12610  ..^cfzo 13690  Σcsu 15718  pmTrspcpmtr 19473  reprcrepr 34601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-pmtr 19474  df-repr 34602
This theorem is referenced by:  hgt750lema  34650
  Copyright terms: Public domain W3C validator