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	⊢ ( 𝜑 → 𝑆 ∈ ℕ₀ )
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	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → 𝑆 ∈ ℕ₀ )
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 ‘ 𝑆 ) 𝑀 ) ) → 𝑆 ∈ ℕ₀ )
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→ 𝑂 )

Metamath Proof Explorer

Theorem reprpmtf1o

Proof