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

Theorem reprpmtf1o 32019
 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 2798 . . . . 5 (𝐴m (0..^𝑆)) = (𝐴m (0..^𝑆))
2 eqid 2798 . . . . 5 (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) = (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇))
3 ovexd 7170 . . . . 5 (𝜑 → (0..^𝑆) ∈ V)
4 nnex 11633 . . . . . . 7 ℕ ∈ V
54a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
6 reprpmtf1o.a . . . . . 6 (𝜑𝐴 ⊆ ℕ)
75, 6ssexd 5192 . . . . 5 (𝜑𝐴 ∈ V)
8 reprpmtf1o.x . . . . . 6 (𝜑𝑋 ∈ (0..^𝑆))
9 reprpmtf1o.s . . . . . . 7 (𝜑𝑆 ∈ ℕ)
10 lbfzo0 13074 . . . . . . 7 (0 ∈ (0..^𝑆) ↔ 𝑆 ∈ ℕ)
119, 10sylibr 237 . . . . . 6 (𝜑 → 0 ∈ (0..^𝑆))
12 reprpmtf1o.t . . . . . 6 𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0}))
133, 8, 11, 12pmtridf1o 30793 . . . . 5 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141, 1, 2, 3, 3, 7, 13fmptco1f1o 30399 . . . 4 (𝜑 → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1-onto→(𝐴m (0..^𝑆)))
15 f1of1 6589 . . . 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 4007 . . . . . 6 {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ⊆ (𝐴m (0..^𝑆))
18 reprpmtf1o.p . . . . . . . . . 10 𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵}
1918ssrab3 4008 . . . . . . . . 9 𝑃 ⊆ (𝐴(repr‘𝑆)𝑀)
2019a1i 11 . . . . . . . 8 (𝜑𝑃 ⊆ (𝐴(repr‘𝑆)𝑀))
21 reprpmtf1o.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
229nnnn0d 11945 . . . . . . . . 9 (𝜑𝑆 ∈ ℕ0)
236, 21, 22reprval 32003 . . . . . . . 8 (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2420, 23sseqtrd 3955 . . . . . . 7 (𝜑𝑃 ⊆ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2524sselda 3915 . . . . . 6 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
2617, 25sseldi 3913 . . . . 5 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴m (0..^𝑆)))
2726ex 416 . . . 4 (𝜑 → (𝑐𝑃𝑐 ∈ (𝐴m (0..^𝑆))))
2827ssrdv 3921 . . 3 (𝜑𝑃 ⊆ (𝐴m (0..^𝑆)))
29 f1ores 6604 . . 3 (((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))–1-1→(𝐴m (0..^𝑆)) ∧ 𝑃 ⊆ (𝐴m (0..^𝑆))) → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
3016, 28, 29syl2anc 587 . 2 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃))
31 resmpt 5872 . . . . 5 (𝑃 ⊆ (𝐴m (0..^𝑆)) → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
3228, 31syl 17 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = (𝑐𝑃 ↦ (𝑐𝑇)))
33 reprpmtf1o.f . . . 4 𝐹 = (𝑐𝑃 ↦ (𝑐𝑇))
3432, 33eqtr4di 2851 . . 3 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃) = 𝐹)
35 eqidd 2799 . . 3 (𝜑𝑃 = 𝑃)
36 vex 3444 . . . . . . . . 9 𝑑 ∈ V
3736a1i 11 . . . . . . . 8 (𝜑𝑑 ∈ V)
382, 37, 28elimampt 30404 . . . . . . 7 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ ∃𝑐𝑃 𝑑 = (𝑐𝑇)))
39 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 = (𝑐𝑇))
40 f1of 6590 . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))⟶(𝐴m (0..^𝑆)))
432fmpt 6851 . . . . . . . . . . . . . . 15 (∀𝑐 ∈ (𝐴m (0..^𝑆))(𝑐𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)):(𝐴m (0..^𝑆))⟶(𝐴m (0..^𝑆)))
4442, 43sylibr 237 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ∀𝑐 ∈ (𝐴m (0..^𝑆))(𝑐𝑇) ∈ (𝐴m (0..^𝑆)))
4526adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑐 ∈ (𝐴m (0..^𝑆)))
46 rspa 3171 . . . . . . . . . . . . . 14 ((∀𝑐 ∈ (𝐴m (0..^𝑆))(𝑐𝑇) ∈ (𝐴m (0..^𝑆)) ∧ 𝑐 ∈ (𝐴m (0..^𝑆))) → (𝑐𝑇) ∈ (𝐴m (0..^𝑆)))
4744, 45, 46syl2anc 587 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐𝑇) ∈ (𝐴m (0..^𝑆)))
4839, 47eqeltrd 2890 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴m (0..^𝑆)))
4939adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = (𝑐𝑇))
5049fveq1d 6647 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = ((𝑐𝑇)‘𝑎))
51 f1ofun 6592 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
5213, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝑇)
5352ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
54 simpr 488 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
55 f1odm 6594 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
5613, 55syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝑇 = (0..^𝑆))
5756ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
5854, 57eleqtrrd 2893 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
59 fvco 6736 . . . . . . . . . . . . . . . . 17 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6053, 58, 59syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6160adantlr 714 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐𝑇)‘𝑎) = (𝑐‘(𝑇𝑎)))
6250, 61eqtrd 2833 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = (𝑐‘(𝑇𝑎)))
6362sumeq2dv 15054 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
64 fveq2 6645 . . . . . . . . . . . . . . 15 (𝑏 = (𝑇𝑎) → (𝑐𝑏) = (𝑐‘(𝑇𝑎)))
65 fzofi 13339 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (0..^𝑆) ∈ Fin)
6713adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
68 eqidd 2799 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
696ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
706adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝐴 ⊆ ℕ)
7121adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑀 ∈ ℤ)
7222adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑆 ∈ ℕ0)
7320sselda 3915 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝑃) → 𝑐 ∈ (𝐴(repr‘𝑆)𝑀))
7470, 71, 72, 73reprf 32005 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝑃) → 𝑐:(0..^𝑆)⟶𝐴)
7574ffvelrnda 6828 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ 𝐴)
7669, 75sseldd 3916 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℕ)
7776nncnd 11643 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐𝑏) ∈ ℂ)
7864, 66, 67, 68, 77fsumf1o 15074 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
7978adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇𝑎)))
8070, 71, 72, 73reprsum 32006 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8180adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐𝑏) = 𝑀)
8263, 79, 813eqtr2d 2839 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀)
83 fveq1 6644 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
8483sumeq2sdv 15055 . . . . . . . . . . . . . 14 (𝑐 = 𝑑 → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎))
8584eqeq1d 2800 . . . . . . . . . . . . 13 (𝑐 = 𝑑 → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8685elrab 3628 . . . . . . . . . . . 12 (𝑑 ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ (𝑑 ∈ (𝐴m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = 𝑀))
8748, 82, 86sylanbrc 586 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8823ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
8987, 88eleqtrrd 2893 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
9039fveq1d 6647 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑‘0) = ((𝑐𝑇)‘0))
9152ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → Fun 𝑇)
9211, 56eleqtrrd 2893 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ dom 𝑇)
9392ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → 0 ∈ dom 𝑇)
94 fvco 6736 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ 0 ∈ dom 𝑇) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
9591, 93, 94syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ((𝑐𝑇)‘0) = (𝑐‘(𝑇‘0)))
963, 8, 11, 12pmtridfv2 30795 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇‘0) = 𝑋)
9796ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑇‘0) = 𝑋)
9897fveq2d 6649 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑐‘(𝑇‘0)) = (𝑐𝑋))
99 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝑃) → 𝑐𝑃)
10099, 18eleqtrdi 2900 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
101 rabid 3331 . . . . . . . . . . . . . . . 16 (𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
102100, 101sylib 221 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑃) → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐𝑋) ∈ 𝐵))
103102simprd 499 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑃) → ¬ (𝑐𝑋) ∈ 𝐵)
104103adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐𝑋) ∈ 𝐵)
10598, 104eqneltrd 2909 . . . . . . . . . . . 12 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑐‘(𝑇‘0)) ∈ 𝐵)
10695, 105eqneltrd 2909 . . . . . . . . . . 11 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ ((𝑐𝑇)‘0) ∈ 𝐵)
10790, 106eqneltrd 2909 . . . . . . . . . 10 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → ¬ (𝑑‘0) ∈ 𝐵)
10889, 107jca 515 . . . . . . . . 9 (((𝜑𝑐𝑃) ∧ 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
109108r19.29an 3247 . . . . . . . 8 ((𝜑 ∧ ∃𝑐𝑃 𝑑 = (𝑐𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
1106adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝐴 ⊆ ℕ)
11121adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑀 ∈ ℤ)
11222adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑆 ∈ ℕ0)
113 simpr 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀))
114110, 111, 112, 113reprf 32005 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑:(0..^𝑆)⟶𝐴)
115 f1ocnv 6602 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
116 f1of 6590 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
11713, 115, 1163syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)⟶(0..^𝑆))
118117adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)⟶(0..^𝑆))
119 fco 6505 . . . . . . . . . . . . . . . . 17 ((𝑑:(0..^𝑆)⟶𝐴𝑇:(0..^𝑆)⟶(0..^𝑆)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
120114, 118, 119syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇):(0..^𝑆)⟶𝐴)
121 elmapg 8404 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
1227, 3, 121syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
123122adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ↔ (𝑑𝑇):(0..^𝑆)⟶𝐴))
124120, 123mpbird 260 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑𝑇) ∈ (𝐴m (0..^𝑆)))
125124adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴m (0..^𝑆)))
126 f1ofun 6592 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇)
12713, 115, 1263syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → Fun 𝑇)
128127ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇)
129 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
130 f1odm 6594 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆))
13113, 115, 1303syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝑇 = (0..^𝑆))
132131adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆))
133129, 132eleqtrrd 2893 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
134133adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇)
135 fvco 6736 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑇𝑎 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
136128, 134, 135syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑑𝑇)‘𝑎) = (𝑑‘(𝑇𝑎)))
137136sumeq2dv 15054 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
138 fveq2 6645 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑇𝑎) → (𝑑𝑏) = (𝑑‘(𝑇𝑎)))
13965a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (0..^𝑆) ∈ Fin)
14013, 115syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
141140adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆))
142 eqidd 2799 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇𝑎) = (𝑇𝑎))
143110adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ)
144114ffvelrnda 6828 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ 𝐴)
145143, 144sseldd 3916 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℕ)
146145nncnd 11643 . . . . . . . . . . . . . . . . 17 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑𝑏) ∈ ℂ)
147138, 139, 141, 142, 146fsumf1o 15074 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(𝑇𝑎)))
148110, 111, 112, 113reprsum 32006 . . . . . . . . . . . . . . . 16 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑𝑏) = 𝑀)
149137, 147, 1483eqtr2d 2839 . . . . . . . . . . . . . . 15 ((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
150149adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀)
151 fveq1 6644 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑑𝑇) → (𝑐𝑎) = ((𝑑𝑇)‘𝑎))
152151sumeq2sdv 15055 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑑𝑇) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎))
153152eqeq1d 2800 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
154153elrab 3628 . . . . . . . . . . . . . 14 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀} ↔ ((𝑑𝑇) ∈ (𝐴m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑑𝑇)‘𝑎) = 𝑀))
155125, 150, 154sylanbrc 586 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
15623ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
157155, 156eleqtrrd 2893 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀))
158127ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Fun 𝑇)
1598, 131eleqtrrd 2893 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ dom 𝑇)
160159ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → 𝑋 ∈ dom 𝑇)
161 fvco 6736 . . . . . . . . . . . . . 14 ((Fun 𝑇𝑋 ∈ dom 𝑇) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
162158, 160, 161syl2anc 587 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ((𝑑𝑇)‘𝑋) = (𝑑‘(𝑇𝑋)))
163 f1ocnvfv 7013 . . . . . . . . . . . . . . . . . 18 ((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) → ((𝑇‘0) = 𝑋 → (𝑇𝑋) = 0))
164163imp 410 . . . . . . . . . . . . . . . . 17 (((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) ∧ (𝑇‘0) = 𝑋) → (𝑇𝑋) = 0)
16513, 11, 96, 164syl21anc 836 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇𝑋) = 0)
166165ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑇𝑋) = 0)
167166fveq2d 6649 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑‘(𝑇𝑋)) = (𝑑‘0))
168 simpr 488 . . . . . . . . . . . . . 14 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘0) ∈ 𝐵)
169167, 168eqneltrd 2909 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘(𝑇𝑋)) ∈ 𝐵)
170162, 169eqneltrd 2909 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵)
171 fveq1 6644 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑𝑇) → (𝑐𝑋) = ((𝑑𝑇)‘𝑋))
172171eleq1d 2874 . . . . . . . . . . . . . 14 (𝑐 = (𝑑𝑇) → ((𝑐𝑋) ∈ 𝐵 ↔ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
173172notbid 321 . . . . . . . . . . . . 13 (𝑐 = (𝑑𝑇) → (¬ (𝑐𝑋) ∈ 𝐵 ↔ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
174173elrab 3628 . . . . . . . . . . . 12 ((𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵} ↔ ((𝑑𝑇) ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ ((𝑑𝑇)‘𝑋) ∈ 𝐵))
175157, 170, 174sylanbrc 586 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵})
176175, 18eleqtrrdi 2901 . . . . . . . . . 10 (((𝜑𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑𝑇) ∈ 𝑃)
177176anasss 470 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑𝑇) ∈ 𝑃)
178 simpr 488 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → 𝑐 = (𝑑𝑇))
179178coeq1d 5696 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑐𝑇) = ((𝑑𝑇) ∘ 𝑇))
180179eqeq2d 2809 . . . . . . . . 9 (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑𝑇)) → (𝑑 = (𝑐𝑇) ↔ 𝑑 = ((𝑑𝑇) ∘ 𝑇)))
181 f1ococnv1 6618 . . . . . . . . . . . . . 14 (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
18213, 181syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
183182adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑇𝑇) = ( I ↾ (0..^𝑆)))
184183coeq2d 5697 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ (𝑇𝑇)) = (𝑑 ∘ ( I ↾ (0..^𝑆))))
185114adantrr 716 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑:(0..^𝑆)⟶𝐴)
186 fcoi1 6526 . . . . . . . . . . . 12 (𝑑:(0..^𝑆)⟶𝐴 → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
187185, 186syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑)
188184, 187eqtr2d 2834 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = (𝑑 ∘ (𝑇𝑇)))
189 coass 6085 . . . . . . . . . 10 ((𝑑𝑇) ∘ 𝑇) = (𝑑 ∘ (𝑇𝑇))
190188, 189eqtr4di 2851 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = ((𝑑𝑇) ∘ 𝑇))
191177, 180, 190rspcedvd 3574 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → ∃𝑐𝑃 𝑑 = (𝑐𝑇))
192109, 191impbida 800 . . . . . . 7 (𝜑 → (∃𝑐𝑃 𝑑 = (𝑐𝑇) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
19338, 192bitrd 282 . . . . . 6 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)))
194 fveq1 6644 . . . . . . . . 9 (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0))
195194eleq1d 2874 . . . . . . . 8 (𝑐 = 𝑑 → ((𝑐‘0) ∈ 𝐵 ↔ (𝑑‘0) ∈ 𝐵))
196195notbid 321 . . . . . . 7 (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ 𝐵 ↔ ¬ (𝑑‘0) ∈ 𝐵))
197196elrab 3628 . . . . . 6 (𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵} ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))
198193, 197bitr4di 292 . . . . 5 (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}))
199198eqrdv 2796 . . . 4 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵})
200 reprpmtf1o.o . . . 4 𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}
201199, 200eqtr4di 2851 . . 3 (𝜑 → ((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) = 𝑂)
20234, 35, 201f1oeq123d 6585 . 2 (𝜑 → (((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) ↾ 𝑃):𝑃1-1-onto→((𝑐 ∈ (𝐴m (0..^𝑆)) ↦ (𝑐𝑇)) “ 𝑃) ↔ 𝐹:𝑃1-1-onto𝑂))
20330, 202mpbid 235 1 (𝜑𝐹:𝑃1-1-onto𝑂)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ⊆ wss 3881  ifcif 4425  {cpr 4527   ↦ cmpt 5110   I cid 5424  ◡ccnv 5518  dom cdm 5519   ↾ cres 5521   “ cima 5522   ∘ ccom 5523  Fun wfun 6318  ⟶wf 6320  –1-1→wf1 6321  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135   ↑m cmap 8391  Fincfn 8494  0cc0 10528  ℕcn 11627  ℕ0cn0 11887  ℤcz 11971  ..^cfzo 13030  Σcsu 15036  pmTrspcpmtr 18564  reprcrepr 32001 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-2o 8088  df-oadd 8091  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-sup 8892  df-oi 8960  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-n0 11888  df-z 11972  df-uz 12234  df-rp 12380  df-fz 12888  df-fzo 13031  df-seq 13367  df-exp 13428  df-hash 13689  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-sum 15037  df-pmtr 18565  df-repr 32002 This theorem is referenced by:  hgt750lema  32050
 Copyright terms: Public domain W3C validator