Metamath Proof Explorer

Theorem reprpmtf1o

Description: Transposing 0 and X maps representations with a condition on the first index to transpositions with the same condition on the index X . (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses 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 reprpmtf1o ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑂 )

Proof

Step Hyp Ref Expression
1 reprpmtf1o.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
2 reprpmtf1o.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 reprpmtf1o.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
4 reprpmtf1o.x ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝑆 ) )
5 reprpmtf1o.o ⊢ 𝑂 = { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ 𝐵 }
6 reprpmtf1o.p ⊢ 𝑃 = { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 }
7 reprpmtf1o.t ⊢ 𝑇 = if ( 𝑋 = 0 , ( I ↾ ( 0 ..^ 𝑆 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 𝑆 ) ) ‘ { 𝑋 , 0 } ) )
8 reprpmtf1o.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑃 ↦ ( 𝑐 ∘ 𝑇 ) )
9 eqid ⊢ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) = ( 𝐴 ↑m ( 0 ..^ 𝑆 ) )
10 eqid ⊢ ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) = ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) )
11 ovexd ⊢ ( 𝜑 → ( 0 ..^ 𝑆 ) ∈ V )
12 nnex ⊢ ℕ ∈ V
13 12 a1i ⊢ ( 𝜑 → ℕ ∈ V )
14 13 3 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
15 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑆 ) ↔ 𝑆 ∈ ℕ )
16 1 15 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑆 ) )
17 11 4 16 7 pmtridf1o ⊢ ( 𝜑 → 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) )
18 9 9 10 11 11 14 17 fmptco1f1o ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) –1-1-onto→ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
19 f1of1 ⊢ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) –1-1-onto→ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) –1-1→ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
20 18 19 syl ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) –1-1→ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
21 ssrab2 ⊢ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ⊆ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) )
22 6 ssrab3 ⊢ 𝑃 ⊆ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 )
23 22 a1i ⊢ ( 𝜑 → 𝑃 ⊆ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
24 1 nnnn0d ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
25 3 2 24 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
26 23 25 sseqtrd ⊢ ( 𝜑 → 𝑃 ⊆ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
27 26 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑐 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
28 21 27 sselid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
29 28 ex ⊢ ( 𝜑 → ( 𝑐 ∈ 𝑃 → 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) )
30 29 ssrdv ⊢ ( 𝜑 → 𝑃 ⊆ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
31 f1ores ⊢ ( ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) –1-1→ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ 𝑃 ⊆ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) ↾ 𝑃 ) : 𝑃 –1-1-onto→ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) )
32 20 30 31 syl2anc ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) ↾ 𝑃 ) : 𝑃 –1-1-onto→ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) )
33 resmpt ⊢ ( 𝑃 ⊆ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) ↾ 𝑃 ) = ( 𝑐 ∈ 𝑃 ↦ ( 𝑐 ∘ 𝑇 ) ) )
34 30 33 syl ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) ↾ 𝑃 ) = ( 𝑐 ∈ 𝑃 ↦ ( 𝑐 ∘ 𝑇 ) ) )
35 34 8 eqtr4di ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) ↾ 𝑃 ) = 𝐹 )
36 eqidd ⊢ ( 𝜑 → 𝑃 = 𝑃 )
37 vex ⊢ 𝑑 ∈ V
38 37 a1i ⊢ ( 𝜑 → 𝑑 ∈ V )
39 10 38 30 elimampt ⊢ ( 𝜑 → ( 𝑑 ∈ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) ↔ ∃ 𝑐 ∈ 𝑃 𝑑 = ( 𝑐 ∘ 𝑇 ) ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → 𝑑 = ( 𝑐 ∘ 𝑇 ) )
41 f1of ⊢ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) –1-1-onto→ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ⟶ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
42 18 41 syl ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ⟶ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ⟶ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
44 10 fmpt ⊢ ( ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ( 𝑐 ∘ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) : ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ⟶ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
45 43 44 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ( 𝑐 ∘ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
46 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
47 rspa ⊢ ( ( ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ( 𝑐 ∘ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( 𝑐 ∘ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
48 45 46 47 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝑐 ∘ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
49 40 48 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
50 40 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑑 = ( 𝑐 ∘ 𝑇 ) )
51 50 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ‘ 𝑎 ) = ( ( 𝑐 ∘ 𝑇 ) ‘ 𝑎 ) )
52 f1ofun ⊢ ( 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) → Fun 𝑇 )
53 17 52 syl ⊢ ( 𝜑 → Fun 𝑇 )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → Fun 𝑇 )
55 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
56 f1odm ⊢ ( 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) → dom 𝑇 = ( 0 ..^ 𝑆 ) )
57 17 56 syl ⊢ ( 𝜑 → dom 𝑇 = ( 0 ..^ 𝑆 ) )
58 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → dom 𝑇 = ( 0 ..^ 𝑆 ) )
59 55 58 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ dom 𝑇 )
60 fvco ⊢ ( ( Fun 𝑇 ∧ 𝑎 ∈ dom 𝑇 ) → ( ( 𝑐 ∘ 𝑇 ) ‘ 𝑎 ) = ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
61 54 59 60 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑐 ∘ 𝑇 ) ‘ 𝑎 ) = ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
62 61 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑐 ∘ 𝑇 ) ‘ 𝑎 ) = ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
63 51 62 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ‘ 𝑎 ) = ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
64 63 sumeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
65 fveq2 ⊢ ( 𝑏 = ( 𝑇 ‘ 𝑎 ) → ( 𝑐 ‘ 𝑏 ) = ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
66 fzofi ⊢ ( 0 ..^ 𝑆 ) ∈ Fin
67 66 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → ( 0 ..^ 𝑆 ) ∈ Fin )
68 17 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) )
69 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑎 ) )
70 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℕ )
71 3 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝐴 ⊆ ℕ )
72 2 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑀 ∈ ℤ )
73 24 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑆 ∈ ℕ0 )
74 23 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
75 71 72 73 74 reprf ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
76 75 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑏 ) ∈ 𝐴 )
77 70 76 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑏 ) ∈ ℕ )
78 77 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑏 ) ∈ ℂ )
79 65 67 68 69 78 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → Σ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑏 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → Σ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑏 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ ( 𝑇 ‘ 𝑎 ) ) )
81 71 72 73 74 reprsum ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → Σ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑏 ) = 𝑀 )
82 81 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → Σ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑏 ) = 𝑀 )
83 64 80 82 3eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 )
84 fveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 𝑎 ) = ( 𝑑 ‘ 𝑎 ) )
85 84 sumeq2sdv ⊢ ( 𝑐 = 𝑑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) )
86 85 eqeq1d ⊢ ( 𝑐 = 𝑑 → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) )
87 86 elrab ⊢ ( 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ↔ ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) )
88 49 83 87 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
89 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
90 88 89 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
91 40 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝑑 ‘ 0 ) = ( ( 𝑐 ∘ 𝑇 ) ‘ 0 ) )
92 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → Fun 𝑇 )
93 16 57 eleqtrrd ⊢ ( 𝜑 → 0 ∈ dom 𝑇 )
94 93 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → 0 ∈ dom 𝑇 )
95 fvco ⊢ ( ( Fun 𝑇 ∧ 0 ∈ dom 𝑇 ) → ( ( 𝑐 ∘ 𝑇 ) ‘ 0 ) = ( 𝑐 ‘ ( 𝑇 ‘ 0 ) ) )
96 92 94 95 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( ( 𝑐 ∘ 𝑇 ) ‘ 0 ) = ( 𝑐 ‘ ( 𝑇 ‘ 0 ) ) )
97 11 4 16 7 pmtridfv2 ⊢ ( 𝜑 → ( 𝑇 ‘ 0 ) = 𝑋 )
98 97 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝑇 ‘ 0 ) = 𝑋 )
99 98 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝑐 ‘ ( 𝑇 ‘ 0 ) ) = ( 𝑐 ‘ 𝑋 ) )
100 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑐 ∈ 𝑃 )
101 100 6 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑐 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 } )
102 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 } ↔ ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 ) )
103 101 102 sylib ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 ) )
104 103 simprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 )
105 104 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 )
106 99 105 eqneltrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ¬ ( 𝑐 ‘ ( 𝑇 ‘ 0 ) ) ∈ 𝐵 )
107 96 106 eqneltrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ¬ ( ( 𝑐 ∘ 𝑇 ) ‘ 0 ) ∈ 𝐵 )
108 91 107 eqneltrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 )
109 90 108 jca ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) )
110 109 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑐 ∈ 𝑃 𝑑 = ( 𝑐 ∘ 𝑇 ) ) → ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) )
111 3 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝐴 ⊆ ℕ )
112 2 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑀 ∈ ℤ )
113 24 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑆 ∈ ℕ0 )
114 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
115 111 112 113 114 reprf ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
116 f1ocnv ⊢ ( 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) → ◡ 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) )
117 f1of ⊢ ( ◡ 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) → ◡ 𝑇 : ( 0 ..^ 𝑆 ) ⟶ ( 0 ..^ 𝑆 ) )
118 17 116 117 3syl ⊢ ( 𝜑 → ◡ 𝑇 : ( 0 ..^ 𝑆 ) ⟶ ( 0 ..^ 𝑆 ) )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ◡ 𝑇 : ( 0 ..^ 𝑆 ) ⟶ ( 0 ..^ 𝑆 ) )
120 fco ⊢ ( ( 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ∧ ◡ 𝑇 : ( 0 ..^ 𝑆 ) ⟶ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ∘ ◡ 𝑇 ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
121 115 119 120 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 𝑑 ∘ ◡ 𝑇 ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
122 elmapg ⊢ ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑑 ∘ ◡ 𝑇 ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
123 14 11 122 syl2anc ⊢ ( 𝜑 → ( ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑑 ∘ ◡ 𝑇 ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑑 ∘ ◡ 𝑇 ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
125 121 124 mpbird ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
126 125 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
127 f1ofun ⊢ ( ◡ 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) → Fun ◡ 𝑇 )
128 17 116 127 3syl ⊢ ( 𝜑 → Fun ◡ 𝑇 )
129 128 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → Fun ◡ 𝑇 )
130 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
131 f1odm ⊢ ( ◡ 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) → dom ◡ 𝑇 = ( 0 ..^ 𝑆 ) )
132 17 116 131 3syl ⊢ ( 𝜑 → dom ◡ 𝑇 = ( 0 ..^ 𝑆 ) )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → dom ◡ 𝑇 = ( 0 ..^ 𝑆 ) )
134 130 133 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ dom ◡ 𝑇 )
135 134 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ dom ◡ 𝑇 )
136 fvco ⊢ ( ( Fun ◡ 𝑇 ∧ 𝑎 ∈ dom ◡ 𝑇 ) → ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) = ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑎 ) ) )
137 129 135 136 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) = ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑎 ) ) )
138 137 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑎 ) ) )
139 fveq2 ⊢ ( 𝑏 = ( ◡ 𝑇 ‘ 𝑎 ) → ( 𝑑 ‘ 𝑏 ) = ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑎 ) ) )
140 66 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
141 17 116 syl ⊢ ( 𝜑 → ◡ 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) )
142 141 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ◡ 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) )
143 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ◡ 𝑇 ‘ 𝑎 ) = ( ◡ 𝑇 ‘ 𝑎 ) )
144 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℕ )
145 115 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ‘ 𝑏 ) ∈ 𝐴 )
146 144 145 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ‘ 𝑏 ) ∈ ℕ )
147 146 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ‘ 𝑏 ) ∈ ℂ )
148 139 140 142 143 147 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → Σ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑏 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑎 ) ) )
149 111 112 113 114 reprsum ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → Σ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑏 ) = 𝑀 )
150 138 148 149 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) = 𝑀 )
151 150 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) = 𝑀 )
152 fveq1 ⊢ ( 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) → ( 𝑐 ‘ 𝑎 ) = ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) )
153 152 sumeq2sdv ⊢ ( 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) )
154 153 eqeq1d ⊢ ( 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) = 𝑀 ) )
155 154 elrab ⊢ ( ( 𝑑 ∘ ◡ 𝑇 ) ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ↔ ( ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑎 ) = 𝑀 ) )
156 126 151 155 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( 𝑑 ∘ ◡ 𝑇 ) ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
157 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
158 156 157 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
159 128 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → Fun ◡ 𝑇 )
160 4 132 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ dom ◡ 𝑇 )
161 160 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → 𝑋 ∈ dom ◡ 𝑇 )
162 fvco ⊢ ( ( Fun ◡ 𝑇 ∧ 𝑋 ∈ dom ◡ 𝑇 ) → ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑋 ) = ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑋 ) ) )
163 159 161 162 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑋 ) = ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑋 ) ) )
164 f1ocnvfv ⊢ ( ( 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) ∧ 0 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑇 ‘ 0 ) = 𝑋 → ( ◡ 𝑇 ‘ 𝑋 ) = 0 ) )
165 164 imp ⊢ ( ( ( 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) ∧ 0 ∈ ( 0 ..^ 𝑆 ) ) ∧ ( 𝑇 ‘ 0 ) = 𝑋 ) → ( ◡ 𝑇 ‘ 𝑋 ) = 0 )
166 17 16 97 165 syl21anc ⊢ ( 𝜑 → ( ◡ 𝑇 ‘ 𝑋 ) = 0 )
167 166 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( ◡ 𝑇 ‘ 𝑋 ) = 0 )
168 167 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑋 ) ) = ( 𝑑 ‘ 0 ) )
169 simpr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 )
170 168 169 eqneltrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ¬ ( 𝑑 ‘ ( ◡ 𝑇 ‘ 𝑋 ) ) ∈ 𝐵 )
171 163 170 eqneltrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ¬ ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑋 ) ∈ 𝐵 )
172 fveq1 ⊢ ( 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) → ( 𝑐 ‘ 𝑋 ) = ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑋 ) )
173 172 eleq1d ⊢ ( 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) → ( ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 ↔ ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑋 ) ∈ 𝐵 ) )
174 173 notbid ⊢ ( 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) → ( ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 ↔ ¬ ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑋 ) ∈ 𝐵 ) )
175 174 elrab ⊢ ( ( 𝑑 ∘ ◡ 𝑇 ) ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 } ↔ ( ( 𝑑 ∘ ◡ 𝑇 ) ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( ( 𝑑 ∘ ◡ 𝑇 ) ‘ 𝑋 ) ∈ 𝐵 ) )
176 158 171 175 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( 𝑑 ∘ ◡ 𝑇 ) ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑋 ) ∈ 𝐵 } )
177 176 6 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) → ( 𝑑 ∘ ◡ 𝑇 ) ∈ 𝑃 )
178 177 anasss ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → ( 𝑑 ∘ ◡ 𝑇 ) ∈ 𝑃 )
179 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) ∧ 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) ) → 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) )
180 179 coeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) ∧ 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) ) → ( 𝑐 ∘ 𝑇 ) = ( ( 𝑑 ∘ ◡ 𝑇 ) ∘ 𝑇 ) )
181 180 eqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) ∧ 𝑐 = ( 𝑑 ∘ ◡ 𝑇 ) ) → ( 𝑑 = ( 𝑐 ∘ 𝑇 ) ↔ 𝑑 = ( ( 𝑑 ∘ ◡ 𝑇 ) ∘ 𝑇 ) ) )
182 f1ococnv1 ⊢ ( 𝑇 : ( 0 ..^ 𝑆 ) –1-1-onto→ ( 0 ..^ 𝑆 ) → ( ◡ 𝑇 ∘ 𝑇 ) = ( I ↾ ( 0 ..^ 𝑆 ) ) )
183 17 182 syl ⊢ ( 𝜑 → ( ◡ 𝑇 ∘ 𝑇 ) = ( I ↾ ( 0 ..^ 𝑆 ) ) )
184 183 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → ( ◡ 𝑇 ∘ 𝑇 ) = ( I ↾ ( 0 ..^ 𝑆 ) ) )
185 184 coeq2d ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → ( 𝑑 ∘ ( ◡ 𝑇 ∘ 𝑇 ) ) = ( 𝑑 ∘ ( I ↾ ( 0 ..^ 𝑆 ) ) ) )
186 115 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
187 fcoi1 ⊢ ( 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 → ( 𝑑 ∘ ( I ↾ ( 0 ..^ 𝑆 ) ) ) = 𝑑 )
188 186 187 syl ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → ( 𝑑 ∘ ( I ↾ ( 0 ..^ 𝑆 ) ) ) = 𝑑 )
189 185 188 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → 𝑑 = ( 𝑑 ∘ ( ◡ 𝑇 ∘ 𝑇 ) ) )
190 coass ⊢ ( ( 𝑑 ∘ ◡ 𝑇 ) ∘ 𝑇 ) = ( 𝑑 ∘ ( ◡ 𝑇 ∘ 𝑇 ) )
191 189 190 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → 𝑑 = ( ( 𝑑 ∘ ◡ 𝑇 ) ∘ 𝑇 ) )
192 178 181 191 rspcedvd ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) → ∃ 𝑐 ∈ 𝑃 𝑑 = ( 𝑐 ∘ 𝑇 ) )
193 110 192 impbida ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝑃 𝑑 = ( 𝑐 ∘ 𝑇 ) ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) )
194 39 193 bitrd ⊢ ( 𝜑 → ( 𝑑 ∈ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) ) )
195 fveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) )
196 195 eleq1d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ 0 ) ∈ 𝐵 ↔ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) )
197 196 notbid ⊢ ( 𝑐 = 𝑑 → ( ¬ ( 𝑐 ‘ 0 ) ∈ 𝐵 ↔ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) )
198 197 elrab ⊢ ( 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ 𝐵 } ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 0 ) ∈ 𝐵 ) )
199 194 198 bitr4di ⊢ ( 𝜑 → ( 𝑑 ∈ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) ↔ 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ 𝐵 } ) )
200 199 eqrdv ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) = { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ 𝐵 } )
201 200 5 eqtr4di ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) = 𝑂 )
202 35 36 201 f1oeq123d ⊢ ( 𝜑 → ( ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) ↾ 𝑃 ) : 𝑃 –1-1-onto→ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↦ ( 𝑐 ∘ 𝑇 ) ) “ 𝑃 ) ↔ 𝐹 : 𝑃 –1-1-onto→ 𝑂 ) )
203 32 202 mpbid ⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑂 )