poimirlem9

Description: Lemma for poimir , establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (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 } ) ) ) ) }
	poimirlem9.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	poimirlem9.2	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
	poimirlem9.3	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	poimirlem9.4	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ≠ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
Assertion	poimirlem9	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 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		poimirlem9.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
4		poimirlem9.2	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
5		poimirlem9.3	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		poimirlem9.4	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ≠ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
7		resundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
8	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
9		npcan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
10	8 9	syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
11	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
12		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
13		uzid	⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
14		peano2uz	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
15	11 12 13 14	4syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
16	10 15	eqeltrrd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
17		fzss2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
18	16 17	syl	⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
19	18 4	sseldd	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... 𝑁 ) )
20		fzp1elp1	⊢ ( ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
21	4 20	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
22	10	oveq2d	⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
23	21 22	eleqtrd	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) )
24	19 23	prssd	⊢ ( 𝜑 → { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) )
25		undif	⊢ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) ↔ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( 1 ... 𝑁 ) )
26	24 25	sylib	⊢ ( 𝜑 → ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( 1 ... 𝑁 ) )
27	26	reseq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( 1 ... 𝑁 ) ) )
28		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 ... 𝑁 ) ) )
29	28 2	eleq2s	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
30		xp1st	⊢ ( 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 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	5 29 30 31	4syl	⊢ ( 𝜑 → ( 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		f1ofn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) )
38		fnresdm	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
39	36 37 38	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
40	27 39	eqtrd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
41	7 40	eqtr3id	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
42		2lt3	⊢ 2 < 3
43		2re	⊢ 2 ∈ ℝ
44		3re	⊢ 3 ∈ ℝ
45	43 44	ltnlei	⊢ ( 2 < 3 ↔ ¬ 3 ≤ 2 )
46	42 45	mpbi	⊢ ¬ 3 ≤ 2
47		df-pr	⊢ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } = ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ∪ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } )
48	47	coeq2i	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ∪ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) )
49		coundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ∪ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) )
50	48 49	eqtri	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) )
51		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 ... 𝑁 ) ) )
52	51 2	eleq2s	⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
53		xp1st	⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
54		xp2nd	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
55	3 52 53 54	4syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
56		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ V
57		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
58	56 57	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
59	55 58	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
60		f1of1	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
61	59 60	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
62	23	snssd	⊢ ( 𝜑 → { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) )
63		f1ores	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ∧ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
64	61 62 63	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
65		f1of	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
66	64 65	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
67		f1ofn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
68	59 67	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
69		fnsnfv	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
70	68 23 69	syl2anc	⊢ ( 𝜑 → { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
71	70	feq3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
72	66 71	mpbird	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } )
73		eqid	⊢ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ }
74		fvex	⊢ ( 2^nd ‘ 𝑇 ) ∈ V
75		ovex	⊢ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ V
76	74 75	fsn	⊢ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } : { ( 2^nd ‘ 𝑇 ) } ⟶ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ↔ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } )
77	73 76	mpbir	⊢ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } : { ( 2^nd ‘ 𝑇 ) } ⟶ { ( ( 2^nd ‘ 𝑇 ) + 1 ) }
78		fco2	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } : { ( 2^nd ‘ 𝑇 ) } ⟶ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } )
79	72 77 78	sylancl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } )
80		fvex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ∈ V
81	80	fconst2	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) = ( { ( 2^nd ‘ 𝑇 ) } × { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ) )
82	79 81	sylib	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) = ( { ( 2^nd ‘ 𝑇 ) } × { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ) )
83	74 80	xpsn	⊢ ( { ( 2^nd ‘ 𝑇 ) } × { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ }
84	82 83	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
85	84	uneq1d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) = ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) )
86	50 85	eqtrid	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) = ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) )
87		elfznn	⊢ ( ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2^nd ‘ 𝑇 ) ∈ ℕ )
88	4 87	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ℕ )
89	88	nnred	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ℝ )
90	89	ltp1d	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) < ( ( 2^nd ‘ 𝑇 ) + 1 ) )
91	89 90	ltned	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ≠ ( ( 2^nd ‘ 𝑇 ) + 1 ) )
92	91	necomd	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) + 1 ) ≠ ( 2^nd ‘ 𝑇 ) )
93		f1veqaeq	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ∧ ( ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) → ( ( 2^nd ‘ 𝑇 ) + 1 ) = ( 2^nd ‘ 𝑇 ) ) )
94	61 23 19 93	syl12anc	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) → ( ( 2^nd ‘ 𝑇 ) + 1 ) = ( 2^nd ‘ 𝑇 ) ) )
95	94	necon3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ 𝑇 ) + 1 ) ≠ ( 2^nd ‘ 𝑇 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ) )
96	92 95	mpd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) )
97	96	neneqd	⊢ ( 𝜑 → ¬ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) )
98	74 80	opth	⊢ ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ ↔ ( ( 2^nd ‘ 𝑇 ) = ( 2^nd ‘ 𝑇 ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ) )
99	98	simprbi	⊢ ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) )
100	97 99	nsyl	⊢ ( 𝜑 → ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ )
101	91	neneqd	⊢ ( 𝜑 → ¬ ( 2^nd ‘ 𝑇 ) = ( ( 2^nd ‘ 𝑇 ) + 1 ) )
102	74 80	opth1	⊢ ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ → ( 2^nd ‘ 𝑇 ) = ( ( 2^nd ‘ 𝑇 ) + 1 ) )
103	101 102	nsyl	⊢ ( 𝜑 → ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ )
104		opex	⊢ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ V
105	104	snid	⊢ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ }
106		elun1	⊢ ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } → ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) )
107	105 106	ax-mp	⊢ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) )
108		eleq2	⊢ ( ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } → ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) ↔ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ) )
109	107 108	mpbii	⊢ ( ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } → ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
110	104	elpr	⊢ ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ↔ ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ ∨ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ) )
111		oran	⊢ ( ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ ∨ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ) ↔ ¬ ( ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ ∧ ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ) )
112	110 111	bitri	⊢ ( ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ∈ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ↔ ¬ ( ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ ∧ ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ) )
113	109 112	sylib	⊢ ( ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } → ¬ ( ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ ∧ ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ) )
114	113	necon2ai	⊢ ( ( ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ ∧ ¬ ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ = ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ ) → ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) ≠ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
115	100 103 114	syl2anc	⊢ ( 𝜑 → ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) ≠ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
116	86 115	eqnetrd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ≠ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
117		fnressn	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) } ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ } )
118	68 19 117	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) } ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ } )
119		fnressn	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
120	68 23 119	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
121	118 120	uneq12d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ } ∪ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ) )
122		df-pr	⊢ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } = ( { ( 2^nd ‘ 𝑇 ) } ∪ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } )
123	122	reseq2i	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) } ∪ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
124		resundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) } ∪ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
125	123 124	eqtri	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
126		df-pr	⊢ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } = ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ } ∪ { ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
127	121 125 126	3eqtr4g	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } )
128	1 2 3 4 5	poimirlem8	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
129		uneq12	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
130		resundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
131	26	reseq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( 1 ... 𝑁 ) ) )
132		fnresdm	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
133	59 67 132	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
134	131 133	eqtrd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
135	130 134	eqtr3id	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
136	41 135	eqeq12d	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
137	129 136	syl5ib	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
138	128 137	mpan2d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
139	138	necon3d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ≠ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
140	6 139	mpd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
141	140	necomd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
142	127 141	eqnetrrd	⊢ ( 𝜑 → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
143		prex	⊢ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ∈ V
144	56 143	coex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ∈ V
145		prex	⊢ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∈ V
146	33	resex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∈ V
147		hashtpg	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ∈ V ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∈ V ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∈ V ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ≠ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) ↔ ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) = 3 ) )
148	144 145 146 147	mp3an	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ≠ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) ↔ ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) = 3 )
149	148	biimpi	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ≠ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) = 3 )
150	149	3expia	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ≠ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) = 3 ) )
151	116 142 150	syl2anc	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) = 3 ) )
152		prex	⊢ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∈ V
153		prex	⊢ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∈ V
154	152 153	mapval	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↑_m { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } }
155		prfi	⊢ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∈ Fin
156		prfi	⊢ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∈ Fin
157		mapfi	⊢ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∈ Fin ∧ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∈ Fin ) → ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↑_m { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∈ Fin )
158	155 156 157	mp2an	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↑_m { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∈ Fin
159	154 158	eqeltrri	⊢ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ∈ Fin
160		f1of	⊢ ( 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } → 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
161	160	ss2abi	⊢ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } }
162		ssfi	⊢ ( ( { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ∈ Fin ∧ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) → { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ∈ Fin )
163	159 161 162	mp2an	⊢ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ∈ Fin
164	23 19	prssd	⊢ ( 𝜑 → { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ⊆ ( 1 ... 𝑁 ) )
165		f1ores	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ∧ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ⊆ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) )
166	61 164 165	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) )
167		fnimapr	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
168	68 23 19 167	syl3anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
169	168	f1oeq3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
170	166 169	mpbid	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
171		f1oprg	⊢ ( ( ( ( 2^nd ‘ 𝑇 ) ∈ V ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ V ) ∧ ( ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ V ∧ ( 2^nd ‘ 𝑇 ) ∈ V ) ) → ( ( ( 2^nd ‘ 𝑇 ) ≠ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ≠ ( 2^nd ‘ 𝑇 ) ) → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) )
172	74 75 75 74 171	mp4an	⊢ ( ( ( 2^nd ‘ 𝑇 ) ≠ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ≠ ( 2^nd ‘ 𝑇 ) ) → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } )
173	91 92 172	syl2anc	⊢ ( 𝜑 → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } )
174		f1oco	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) : { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
175	170 173 174	syl2anc	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
176		rnpropg	⊢ ( ( ( 2^nd ‘ 𝑇 ) ∈ V ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ V ) → ran { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } = { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } )
177	74 75 176	mp2an	⊢ ran { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } = { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) }
178	177	eqimssi	⊢ ran { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ⊆ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) }
179		cores	⊢ ( ran { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ⊆ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) )
180		f1oeq1	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
181	178 179 180	mp2b	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ { ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) } ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
182	175 181	sylib	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
183	96	necomd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) )
184		fvex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ∈ V
185		f1oprg	⊢ ( ( ( ( 2^nd ‘ 𝑇 ) ∈ V ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ∈ V ) ∧ ( ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ V ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ∈ V ) ) → ( ( ( 2^nd ‘ 𝑇 ) ≠ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ) → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ) )
186	74 184 75 80 185	mp4an	⊢ ( ( ( 2^nd ‘ 𝑇 ) ≠ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ) → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } )
187	91 183 186	syl2anc	⊢ ( 𝜑 → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } )
188		prcom	⊢ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) }
189		f1oeq3	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } → ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ↔ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
190	188 189	ax-mp	⊢ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } ↔ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
191	187 190	sylib	⊢ ( 𝜑 → { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
192		f1of1	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
193	36 192	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
194		f1ores	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ∧ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
195	193 24 194	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
196		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ) )
197	196	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
198		imadif	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
199	36 197 198	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
200		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
201		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
202	36 200 201	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
203		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
204		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
205	59 203 204	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
206	202 205	eqtr4d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) )
207	128	rneqd	⊢ ( 𝜑 → ran ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ran ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
208		df-ima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ran ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
209		df-ima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ran ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
210	207 208 209	3eqtr4g	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
211	206 210	difeq12d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
212		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
213	212	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
214		imadif	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
215	59 213 214	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
216		dfin4	⊢ ( ( 1 ... 𝑁 ) ∩ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
217		sseqin2	⊢ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) ↔ ( ( 1 ... 𝑁 ) ∩ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } )
218	24 217	sylib	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } )
219	216 218	eqtr3id	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } )
220	219	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
221	215 220	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
222	199 211 221	3eqtrd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
223	219	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ ( ( 1 ... 𝑁 ) ∖ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
224		fnimapr	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... 𝑁 ) ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } )
225	68 19 23 224	syl3anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) } )
226	225 188	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
227	222 223 226	3eqtr3d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
228	227	f1oeq3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) “ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
229	195 228	mpbid	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
230		ssabral	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ↔ ∀ 𝑓 ∈ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } )
231		f1oeq1	⊢ ( 𝑓 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) → ( 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
232		f1oeq1	⊢ ( 𝑓 = { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } → ( 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↔ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
233		f1oeq1	⊢ ( 𝑓 = ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) → ( 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
234	144 145 146 231 232 233	raltp	⊢ ( ∀ 𝑓 ∈ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ↔ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
235	230 234	bitri	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ↔ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∧ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) )
236	182 191 229 235	syl3anbrc	⊢ ( 𝜑 → { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } )
237		hashss	⊢ ( ( { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ∈ Fin ∧ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) ≤ ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) )
238	163 236 237	sylancr	⊢ ( 𝜑 → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) ≤ ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) )
239	153	enref	⊢ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ≈ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) }
240		hashprg	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ∈ V ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ∈ V ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ↔ ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) = 2 ) )
241	80 184 240	mp2an	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ↔ ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) = 2 )
242	96 241	sylib	⊢ ( 𝜑 → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) = 2 )
243		hashprg	⊢ ( ( ( 2^nd ‘ 𝑇 ) ∈ V ∧ ( ( 2^nd ‘ 𝑇 ) + 1 ) ∈ V ) → ( ( 2^nd ‘ 𝑇 ) ≠ ( ( 2^nd ‘ 𝑇 ) + 1 ) ↔ ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = 2 ) )
244	74 75 243	mp2an	⊢ ( ( 2^nd ‘ 𝑇 ) ≠ ( ( 2^nd ‘ 𝑇 ) + 1 ) ↔ ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = 2 )
245	91 244	sylib	⊢ ( 𝜑 → ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = 2 )
246	242 245	eqtr4d	⊢ ( 𝜑 → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) = ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
247		hashen	⊢ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ∈ Fin ∧ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∈ Fin ) → ( ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) = ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ↔ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ≈ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
248	155 156 247	mp2an	⊢ ( ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ) = ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ↔ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ≈ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } )
249	246 248	sylib	⊢ ( 𝜑 → { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ≈ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } )
250		hashfacen	⊢ ( ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ≈ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∧ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } ≈ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) → { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ≈ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } )
251	239 249 250	sylancr	⊢ ( 𝜑 → { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ≈ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } )
252	153 153	mapval	⊢ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ↑_m { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } }
253		mapfi	⊢ ( ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∈ Fin ∧ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∈ Fin ) → ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ↑_m { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∈ Fin )
254	156 156 253	mp2an	⊢ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ↑_m { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∈ Fin
255	252 254	eqeltrri	⊢ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ∈ Fin
256		f1of	⊢ ( 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } → 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } )
257	256	ss2abi	⊢ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } }
258		ssfi	⊢ ( ( { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ∈ Fin ∧ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ⊆ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ⟶ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) → { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ∈ Fin )
259	255 257 258	mp2an	⊢ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ∈ Fin
260		hashen	⊢ ( ( { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ∈ Fin ∧ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ∈ Fin ) → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) ↔ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ≈ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) )
261	163 259 260	mp2an	⊢ ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) ↔ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ≈ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } )
262	251 261	sylibr	⊢ ( 𝜑 → ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) )
263		hashfac	⊢ ( { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) = ( ! ‘ ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) )
264	156 263	ax-mp	⊢ ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) = ( ! ‘ ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
265	245	fveq2d	⊢ ( 𝜑 → ( ! ‘ ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( ! ‘ 2 ) )
266		fac2	⊢ ( ! ‘ 2 ) = 2
267	265 266	eqtrdi	⊢ ( 𝜑 → ( ! ‘ ( ♯ ‘ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = 2 )
268	264 267	eqtrid	⊢ ( 𝜑 → ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } } ) = 2 )
269	262 268	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ { 𝑓 ∣ 𝑓 : { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) } } ) = 2 )
270	238 269	breqtrd	⊢ ( 𝜑 → ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) ≤ 2 )
271		breq1	⊢ ( ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) = 3 → ( ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) ≤ 2 ↔ 3 ≤ 2 ) )
272	270 271	syl5ibcom	⊢ ( 𝜑 → ( ( ♯ ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) , { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( 2^nd ‘ 𝑇 ) ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ 𝑇 ) + 1 ) ) ⟩ } , ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) } ) = 3 → 3 ≤ 2 ) )
273	151 272	syld	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) → 3 ≤ 2 ) )
274	273	necon1bd	⊢ ( 𝜑 → ( ¬ 3 ≤ 2 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ) )
275	46 274	mpi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) )
276		coires1	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) )
277	128 276	eqtr4di	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
278	275 277	uneq12d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) ) )
279	41 278	eqtr3d	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) ) )
280		coundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) )
281	279 280	eqtr4di	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2^nd ‘ 𝑇 ) + 1 ) , ( 2^nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2^nd ‘ 𝑇 ) , ( ( 2^nd ‘ 𝑇 ) + 1 ) } ) ) ) ) )

Metamath Proof Explorer

Theorem poimirlem9

Proof