poimirlem12

Description: Lemma for poimir connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	poimirlem22.s	⊢ 𝑆 = { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
	poimirlem22.1	⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
	poimirlem12.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	poimirlem12.3	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) = 𝑁 )
	poimirlem12.4	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	poimirlem12.5	⊢ ( 𝜑 → ( 2^nd ‘ 𝑈 ) = 𝑁 )
	poimirlem12.6	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
Assertion	poimirlem12	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ⊆ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		poimirlem22.s	⊢ 𝑆 = { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
3		poimirlem22.1	⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
4		poimirlem12.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5		poimirlem12.3	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) = 𝑁 )
6		poimirlem12.4	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		poimirlem12.5	⊢ ( 𝜑 → ( 2^nd ‘ 𝑈 ) = 𝑁 )
8		poimirlem12.6	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
9		eldif	⊢ ( 𝑦 ∈ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ↔ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) )
10		imassrn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ⊆ ran ( 2^nd ‘ ( 1^st ‘ 𝑇 ) )
11		elrabi	⊢ ( 𝑇 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) } → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
12	11 2	eleq2s	⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
13		xp1st	⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
14	4 12 13	3syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
15		xp2nd	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
16	14 15	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
17		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ V
18		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
19	17 18	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
20	16 19	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
21		f1of	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
22		frn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) → ran ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ⊆ ( 1 ... 𝑁 ) )
23	20 21 22	3syl	⊢ ( 𝜑 → ran ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ⊆ ( 1 ... 𝑁 ) )
24	10 23	sstrid	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ⊆ ( 1 ... 𝑁 ) )
25		elrabi	⊢ ( 𝑈 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) } → 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
26	25 2	eleq2s	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
27		xp1st	⊢ ( 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
28	6 26 27	3syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
29		xp2nd	⊢ ( ( 1^st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
30	28 29	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
31		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ∈ V
32		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
33	31 32	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
34	30 33	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
35		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
36		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
37	34 35 36	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
38	24 37	sseqtrrd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ⊆ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) )
39	38	ssdifd	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ⊆ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) )
40		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ) )
41	40	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
42		imadif	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑀 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) )
43	34 41 42	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑀 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) )
44		difun2	⊢ ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∪ ( 1 ... 𝑀 ) ) ∖ ( 1 ... 𝑀 ) ) = ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∖ ( 1 ... 𝑀 ) )
45		elfznn0	⊢ ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑀 ∈ ℕ₀ )
46		nn0p1nn	⊢ ( 𝑀 ∈ ℕ₀ → ( 𝑀 + 1 ) ∈ ℕ )
47	8 45 46	3syl	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ )
48		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
49	47 48	eleqtrdi	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
50	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
51		npcan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
52	50 51	syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
53		elfzuz3	⊢ ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ 𝑀 ) )
54		peano2uz	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 𝑀 ) )
55	8 53 54	3syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 𝑀 ) )
56	52 55	eqeltrrd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) )
57		fzsplit2	⊢ ( ( ( 𝑀 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
58	49 56 57	syl2anc	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
59		uncom	⊢ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∪ ( 1 ... 𝑀 ) )
60	58 59	eqtrdi	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∪ ( 1 ... 𝑀 ) ) )
61	60	difeq1d	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑀 ) ) = ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∪ ( 1 ... 𝑀 ) ) ∖ ( 1 ... 𝑀 ) ) )
62		incom	⊢ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ( 1 ... 𝑀 ) ) = ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) )
63	8 45	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
64	63	nn0red	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
65	64	ltp1d	⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
66		fzdisj	⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
67	65 66	syl	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
68	62 67	syl5eq	⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ( 1 ... 𝑀 ) ) = ∅ )
69		disj3	⊢ ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ( 1 ... 𝑀 ) ) = ∅ ↔ ( ( 𝑀 + 1 ) ... 𝑁 ) = ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∖ ( 1 ... 𝑀 ) ) )
70	68 69	sylib	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) = ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∖ ( 1 ... 𝑀 ) ) )
71	44 61 70	3eqtr4a	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑀 ) ) = ( ( 𝑀 + 1 ) ... 𝑁 ) )
72	71	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑀 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
73	43 72	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
74	39 73	sseqtrd	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ⊆ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
75	74	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ) → 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
76	9 75	sylan2br	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ) → 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
77		fveq2	⊢ ( 𝑡 = 𝑈 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑈 ) )
78	77	breq2d	⊢ ( 𝑡 = 𝑈 → ( 𝑦 < ( 2^nd ‘ 𝑡 ) ↔ 𝑦 < ( 2^nd ‘ 𝑈 ) ) )
79	78	ifbid	⊢ ( 𝑡 = 𝑈 → if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) )
80	79	csbeq1d	⊢ ( 𝑡 = 𝑈 → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
81		2fveq3	⊢ ( 𝑡 = 𝑈 → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) )
82		2fveq3	⊢ ( 𝑡 = 𝑈 → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
83	82	imaeq1d	⊢ ( 𝑡 = 𝑈 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) )
84	83	xpeq1d	⊢ ( 𝑡 = 𝑈 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
85	82	imaeq1d	⊢ ( 𝑡 = 𝑈 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
86	85	xpeq1d	⊢ ( 𝑡 = 𝑈 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
87	84 86	uneq12d	⊢ ( 𝑡 = 𝑈 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
88	81 87	oveq12d	⊢ ( 𝑡 = 𝑈 → ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
89	88	csbeq2dv	⊢ ( 𝑡 = 𝑈 → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
90	80 89	eqtrd	⊢ ( 𝑡 = 𝑈 → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
91	90	mpteq2dv	⊢ ( 𝑡 = 𝑈 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
92	91	eqeq2d	⊢ ( 𝑡 = 𝑈 → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
93	92 2	elrab2	⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
94	93	simprbi	⊢ ( 𝑈 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
95	6 94	syl	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
96		breq1	⊢ ( 𝑦 = 𝑀 → ( 𝑦 < ( 2^nd ‘ 𝑈 ) ↔ 𝑀 < ( 2^nd ‘ 𝑈 ) ) )
97		id	⊢ ( 𝑦 = 𝑀 → 𝑦 = 𝑀 )
98	96 97	ifbieq1d	⊢ ( 𝑦 = 𝑀 → if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑀 < ( 2^nd ‘ 𝑈 ) , 𝑀 , ( 𝑦 + 1 ) ) )
99	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
100		peano2rem	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
101	99 100	syl	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
102		elfzle2	⊢ ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑀 ≤ ( 𝑁 − 1 ) )
103	8 102	syl	⊢ ( 𝜑 → 𝑀 ≤ ( 𝑁 − 1 ) )
104	99	ltm1d	⊢ ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
105	64 101 99 103 104	lelttrd	⊢ ( 𝜑 → 𝑀 < 𝑁 )
106	105 7	breqtrrd	⊢ ( 𝜑 → 𝑀 < ( 2^nd ‘ 𝑈 ) )
107	106	iftrued	⊢ ( 𝜑 → if ( 𝑀 < ( 2^nd ‘ 𝑈 ) , 𝑀 , ( 𝑦 + 1 ) ) = 𝑀 )
108	98 107	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) = 𝑀 )
109	108	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 𝑀 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
110		oveq2	⊢ ( 𝑗 = 𝑀 → ( 1 ... 𝑗 ) = ( 1 ... 𝑀 ) )
111	110	imaeq2d	⊢ ( 𝑗 = 𝑀 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) )
112	111	xpeq1d	⊢ ( 𝑗 = 𝑀 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) )
113		oveq1	⊢ ( 𝑗 = 𝑀 → ( 𝑗 + 1 ) = ( 𝑀 + 1 ) )
114	113	oveq1d	⊢ ( 𝑗 = 𝑀 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑀 + 1 ) ... 𝑁 ) )
115	114	imaeq2d	⊢ ( 𝑗 = 𝑀 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
116	115	xpeq1d	⊢ ( 𝑗 = 𝑀 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) )
117	112 116	uneq12d	⊢ ( 𝑗 = 𝑀 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
118	117	oveq2d	⊢ ( 𝑗 = 𝑀 → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
119	118	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝑀 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
120	8 119	csbied	⊢ ( 𝜑 → ⦋ 𝑀 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
121	120	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ 𝑀 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
122	109 121	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
123		ovexd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
124	95 122 8 123	fvmptd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
125	124	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) )
126	125	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) )
127		imassrn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ⊆ ran ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
128		f1of	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
129		frn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) → ran ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⊆ ( 1 ... 𝑁 ) )
130	34 128 129	3syl	⊢ ( 𝜑 → ran ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⊆ ( 1 ... 𝑁 ) )
131	127 130	sstrid	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ⊆ ( 1 ... 𝑁 ) )
132	131	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑦 ∈ ( 1 ... 𝑁 ) )
133		xp1st	⊢ ( ( 1^st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
134		elmapfn	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) )
135	28 133 134	3syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) )
136	135	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) )
137		1ex	⊢ 1 ∈ V
138		fnconstg	⊢ ( 1 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) )
139	137 138	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) )
140		c0ex	⊢ 0 ∈ V
141		fnconstg	⊢ ( 0 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
142	140 141	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) )
143	139 142	pm3.2i	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
144		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
145	34 41 144	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
146	67	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ∅ ) )
147		ima0	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ∅ ) = ∅
148	146 147	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
149	145 148	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
150		fnun	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
151	143 149 150	sylancr	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
152		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
153	58	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
154	153 37	eqtr3d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
155	152 154	syl5eqr	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
156	155	fneq2d	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ↔ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
157	151 156	mpbid	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
158	157	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
159		ovexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ V )
160		inidm	⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
161		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) )
162		fvun2	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑦 ) )
163	139 142 162	mp3an12	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑦 ) )
164	149 163	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑦 ) )
165	140	fvconst2	⊢ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑦 ) = 0 )
166	165	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑦 ) = 0 )
167	164 166	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = 0 )
168	167	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = 0 )
169	136 158 159 159 160 161 168	ofval	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) + 0 ) )
170	132 169	mpdan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) + 0 ) )
171		elmapi	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
172	28 133 171	3syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
173	172	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) ∈ ( 0 ..^ 𝐾 ) )
174		elfzonn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) ∈ ℕ₀ )
175	173 174	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) ∈ ℕ₀ )
176	175	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) ∈ ℂ )
177	176	addid1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) + 0 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) )
178	132 177	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) + 0 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) )
179	126 170 178	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) )
180	76 179	syldan	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) )
181		fveq2	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑇 ) )
182	181	breq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑦 < ( 2^nd ‘ 𝑡 ) ↔ 𝑦 < ( 2^nd ‘ 𝑇 ) ) )
183	182	ifbid	⊢ ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
184	183	csbeq1d	⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
185		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) )
186		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
187	186	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
188	187	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
189	186	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
190	189	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
191	188 190	uneq12d	⊢ ( 𝑡 = 𝑇 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
192	185 191	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
193	192	csbeq2dv	⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
194	184 193	eqtrd	⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
195	194	mpteq2dv	⊢ ( 𝑡 = 𝑇 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
196	195	eqeq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
197	196 2	elrab2	⊢ ( 𝑇 ∈ 𝑆 ↔ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
198	197	simprbi	⊢ ( 𝑇 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
199	4 198	syl	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
200		breq1	⊢ ( 𝑦 = 𝑀 → ( 𝑦 < ( 2^nd ‘ 𝑇 ) ↔ 𝑀 < ( 2^nd ‘ 𝑇 ) ) )
201	200 97	ifbieq1d	⊢ ( 𝑦 = 𝑀 → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑀 < ( 2^nd ‘ 𝑇 ) , 𝑀 , ( 𝑦 + 1 ) ) )
202	105 5	breqtrrd	⊢ ( 𝜑 → 𝑀 < ( 2^nd ‘ 𝑇 ) )
203	202	iftrued	⊢ ( 𝜑 → if ( 𝑀 < ( 2^nd ‘ 𝑇 ) , 𝑀 , ( 𝑦 + 1 ) ) = 𝑀 )
204	201 203	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = 𝑀 )
205	204	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 𝑀 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
206	110	imaeq2d	⊢ ( 𝑗 = 𝑀 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) )
207	206	xpeq1d	⊢ ( 𝑗 = 𝑀 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) )
208	114	imaeq2d	⊢ ( 𝑗 = 𝑀 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
209	208	xpeq1d	⊢ ( 𝑗 = 𝑀 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) )
210	207 209	uneq12d	⊢ ( 𝑗 = 𝑀 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
211	210	oveq2d	⊢ ( 𝑗 = 𝑀 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
212	211	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝑀 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
213	8 212	csbied	⊢ ( 𝜑 → ⦋ 𝑀 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
214	213	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ 𝑀 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
215	205 214	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
216		ovexd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
217	199 215 8 216	fvmptd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
218	217	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) )
219	218	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) )
220	24	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → 𝑦 ∈ ( 1 ... 𝑁 ) )
221		xp1st	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
222		elmapfn	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
223	14 221 222	3syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
224	223	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
225		fnconstg	⊢ ( 1 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) )
226	137 225	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) )
227		fnconstg	⊢ ( 0 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
228	140 227	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) )
229	226 228	pm3.2i	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
230		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
231	230	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
232		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
233	20 231 232	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
234	67	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) )
235		ima0	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) = ∅
236	234 235	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
237	233 236	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
238		fnun	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
239	229 237 238	sylancr	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
240		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
241	58	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
242		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
243		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
244	20 242 243	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
245	241 244	eqtr3d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
246	240 245	syl5eqr	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
247	246	fneq2d	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ↔ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
248	239 247	mpbid	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
249	248	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
250		ovexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( 1 ... 𝑁 ) ∈ V )
251		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
252		fvun1	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ 𝑦 ) )
253	226 228 252	mp3an12	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ 𝑦 ) )
254	237 253	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ 𝑦 ) )
255	137	fvconst2	⊢ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ 𝑦 ) = 1 )
256	255	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ 𝑦 ) = 1 )
257	254 256	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = 1 )
258	257	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑦 ) = 1 )
259	224 249 250 250 160 251 258	ofval	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) )
260	220 259	mpdan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) )
261	219 260	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) )
262	261	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑦 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) )
263	1	nngt0d	⊢ ( 𝜑 → 0 < 𝑁 )
264	263 7	breqtrrd	⊢ ( 𝜑 → 0 < ( 2^nd ‘ 𝑈 ) )
265	1 2 6 264	poimirlem5	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) )
266	263 5	breqtrrd	⊢ ( 𝜑 → 0 < ( 2^nd ‘ 𝑇 ) )
267	1 2 4 266	poimirlem5	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) )
268	265 267	eqtr3d	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) )
269	268	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
270	269	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
271	180 262 270	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
272		elmapi	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
273	14 221 272	3syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
274	273	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) ∈ ( 0 ..^ 𝐾 ) )
275		elfzonn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) ∈ ℕ₀ )
276	274 275	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) ∈ ℕ₀ )
277	276	nn0red	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) ∈ ℝ )
278	277	ltp1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) < ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) )
279	277 278	gtned	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) ≠ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
280	220 279	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) ≠ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
281	280	neneqd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ¬ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
282	281	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ) → ¬ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) + 1 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑦 ) )
283	271 282	pm2.65da	⊢ ( 𝜑 → ¬ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) )
284		iman	⊢ ( ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) → 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) ↔ ¬ ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) )
285	283 284	sylibr	⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) → 𝑦 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) ) )
286	285	ssrdv	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ⊆ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑀 ) ) )

Metamath Proof Explorer

Theorem poimirlem12

Proof