finxpsuclem

		Ref	Expression
	Hypothesis	finxpsuclem.1	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
	Assertion	finxpsuclem	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑈 ↑↑ suc 𝑁 ) = ( ( 𝑈 ↑↑ 𝑁 ) × 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		finxpsuclem.1	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
2		peano2	⊢ ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
3	2	adantr	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → suc 𝑁 ∈ ω )
4		1on	⊢ 1_o ∈ On
5	4	onordi	⊢ Ord 1_o
6		nnord	⊢ ( 𝑁 ∈ ω → Ord 𝑁 )
7		ordsseleq	⊢ ( ( Ord 1_o ∧ Ord 𝑁 ) → ( 1_o ⊆ 𝑁 ↔ ( 1_o ∈ 𝑁 ∨ 1_o = 𝑁 ) ) )
8	5 6 7	sylancr	⊢ ( 𝑁 ∈ ω → ( 1_o ⊆ 𝑁 ↔ ( 1_o ∈ 𝑁 ∨ 1_o = 𝑁 ) ) )
9	8	biimpa	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 1_o ∈ 𝑁 ∨ 1_o = 𝑁 ) )
10		elelsuc	⊢ ( 1_o ∈ 𝑁 → 1_o ∈ suc 𝑁 )
11	10	a1i	⊢ ( 𝑁 ∈ ω → ( 1_o ∈ 𝑁 → 1_o ∈ suc 𝑁 ) )
12		sucidg	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ suc 𝑁 )
13		eleq1	⊢ ( 1_o = 𝑁 → ( 1_o ∈ suc 𝑁 ↔ 𝑁 ∈ suc 𝑁 ) )
14	12 13	syl5ibrcom	⊢ ( 𝑁 ∈ ω → ( 1_o = 𝑁 → 1_o ∈ suc 𝑁 ) )
15	11 14	jaod	⊢ ( 𝑁 ∈ ω → ( ( 1_o ∈ 𝑁 ∨ 1_o = 𝑁 ) → 1_o ∈ suc 𝑁 ) )
16	15	adantr	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( ( 1_o ∈ 𝑁 ∨ 1_o = 𝑁 ) → 1_o ∈ suc 𝑁 ) )
17	9 16	mpd	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → 1_o ∈ suc 𝑁 )
18	1	finxpreclem6	⊢ ( ( suc 𝑁 ∈ ω ∧ 1_o ∈ suc 𝑁 ) → ( 𝑈 ↑↑ suc 𝑁 ) ⊆ ( V × 𝑈 ) )
19	3 17 18	syl2anc	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑈 ↑↑ suc 𝑁 ) ⊆ ( V × 𝑈 ) )
20	19	sselda	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ) → 𝑦 ∈ ( V × 𝑈 ) )
21	2	ad2antrr	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → suc 𝑁 ∈ ω )
22		df-2o	⊢ 2_o = suc 1_o
23		ordsucsssuc	⊢ ( ( Ord 1_o ∧ Ord 𝑁 ) → ( 1_o ⊆ 𝑁 ↔ suc 1_o ⊆ suc 𝑁 ) )
24	5 6 23	sylancr	⊢ ( 𝑁 ∈ ω → ( 1_o ⊆ 𝑁 ↔ suc 1_o ⊆ suc 𝑁 ) )
25	24	biimpa	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → suc 1_o ⊆ suc 𝑁 )
26	22 25	eqsstrid	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → 2_o ⊆ suc 𝑁 )
27	26	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → 2_o ⊆ suc 𝑁 )
28		simpr	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → 𝑦 ∈ ( V × 𝑈 ) )
29	1	finxpreclem4	⊢ ( ( ( suc 𝑁 ∈ ω ∧ 2_o ⊆ suc 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) = ( rec ( 𝐹 , ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ ∪ suc 𝑁 ) )
30	21 27 28 29	syl21anc	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) = ( rec ( 𝐹 , ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ ∪ suc 𝑁 ) )
31		ordunisuc	⊢ ( Ord 𝑁 → ∪ suc 𝑁 = 𝑁 )
32	6 31	syl	⊢ ( 𝑁 ∈ ω → ∪ suc 𝑁 = 𝑁 )
33		opeq1	⊢ ( ∪ suc 𝑁 = 𝑁 → ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ = ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ )
34		rdgeq2	⊢ ( ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ = ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ → rec ( 𝐹 , ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) = rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) )
35	33 34	syl	⊢ ( ∪ suc 𝑁 = 𝑁 → rec ( 𝐹 , ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) = rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) )
36	32 35	syl	⊢ ( 𝑁 ∈ ω → rec ( 𝐹 , ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) = rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) )
37	36 32	fveq12d	⊢ ( 𝑁 ∈ ω → ( rec ( 𝐹 , ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ ∪ suc 𝑁 ) = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) )
38	37	ad2antrr	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ ∪ suc 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ ∪ suc 𝑁 ) = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) )
39	30 38	eqtrd	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) )
40	39	eqeq2d	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( ∅ = ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) ) )
41	1	dffinxpf	⊢ ( 𝑈 ↑↑ suc 𝑁 ) = { 𝑦 ∣ ( suc 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) ) }
42	41	abeq2i	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ↔ ( suc 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) ) )
43	2	biantrurd	⊢ ( 𝑁 ∈ ω → ( ∅ = ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) ↔ ( suc 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) ) ) )
44	42 43	bitr4id	⊢ ( 𝑁 ∈ ω → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) ) )
45	44	ad2antrr	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ suc 𝑁 , 𝑦 ⟩ ) ‘ suc 𝑁 ) ) )
46		fvex	⊢ ( 1^st ‘ 𝑦 ) ∈ V
47		opeq2	⊢ ( 𝑧 = ( 1^st ‘ 𝑦 ) → ⟨ 𝑁 , 𝑧 ⟩ = ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ )
48		rdgeq2	⊢ ( ⟨ 𝑁 , 𝑧 ⟩ = ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ → rec ( 𝐹 , ⟨ 𝑁 , 𝑧 ⟩ ) = rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) )
49	47 48	syl	⊢ ( 𝑧 = ( 1^st ‘ 𝑦 ) → rec ( 𝐹 , ⟨ 𝑁 , 𝑧 ⟩ ) = rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) )
50	49	fveq1d	⊢ ( 𝑧 = ( 1^st ‘ 𝑦 ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑧 ⟩ ) ‘ 𝑁 ) = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) )
51	50	eqeq2d	⊢ ( 𝑧 = ( 1^st ‘ 𝑦 ) → ( ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑧 ⟩ ) ‘ 𝑁 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) ) )
52	51	anbi2d	⊢ ( 𝑧 = ( 1^st ‘ 𝑦 ) → ( ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑧 ⟩ ) ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) ) ) )
53	1	dffinxpf	⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑧 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑧 ⟩ ) ‘ 𝑁 ) ) }
54	46 52 53	elab2	⊢ ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ↔ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) ) )
55	54	baib	⊢ ( 𝑁 ∈ ω → ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) ) )
56	55	ad2antrr	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , ( 1^st ‘ 𝑦 ) ⟩ ) ‘ 𝑁 ) ) )
57	40 45 56	3bitr4d	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ↔ ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
58	57	biimpd	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) → ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
59	58	impancom	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ) → ( 𝑦 ∈ ( V × 𝑈 ) → ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
60	20 59	mpd	⊢ ( ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ) → ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) )
61	60	ex	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) → ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
62	20	ex	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) → 𝑦 ∈ ( V × 𝑈 ) ) )
63	61 62	jcad	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) → ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) ) )
64	57	exbiri	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑦 ∈ ( V × 𝑈 ) → ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) → 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ) ) )
65	64	impd	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( ( 𝑦 ∈ ( V × 𝑈 ) ∧ ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ) → 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ) )
66	65	ancomsd	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ) )
67	63 66	impbid	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ↔ ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) ) )
68		elxp8	⊢ ( 𝑦 ∈ ( ( 𝑈 ↑↑ 𝑁 ) × 𝑈 ) ↔ ( ( 1^st ‘ 𝑦 ) ∈ ( 𝑈 ↑↑ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) )
69	67 68	bitr4di	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑦 ∈ ( 𝑈 ↑↑ suc 𝑁 ) ↔ 𝑦 ∈ ( ( 𝑈 ↑↑ 𝑁 ) × 𝑈 ) ) )
70	69	eqrdv	⊢ ( ( 𝑁 ∈ ω ∧ 1_o ⊆ 𝑁 ) → ( 𝑈 ↑↑ suc 𝑁 ) = ( ( 𝑈 ↑↑ 𝑁 ) × 𝑈 ) )

Metamath Proof Explorer

Theorem finxpsuclem

Proof