poimirlem11

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

Metamath Proof Explorer

Theorem poimirlem11

Proof