Theorem finxpreclem4

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 23-Oct-2020)

	Ref	Expression
Hypothesis	finxpreclem4.1	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
Assertion	finxpreclem4	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∪ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		finxpreclem4.1	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
2		2onn	⊢ 2o ∈ ω
3		nnon	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
4		2on	⊢ 2o ∈ On
5		oawordeu	⊢ ( ( ( 2o ∈ On ∧ 𝑁 ∈ On ) ∧ 2o ⊆ 𝑁 ) → ∃! 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 )
6	4 5	mpanl1	⊢ ( ( 𝑁 ∈ On ∧ 2o ⊆ 𝑁 ) → ∃! 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 )
7		riotasbc	⊢ ( ∃! 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 → [ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ] ( 2o +o 𝑜 ) = 𝑁 )
8	6 7	syl	⊢ ( ( 𝑁 ∈ On ∧ 2o ⊆ 𝑁 ) → [ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ] ( 2o +o 𝑜 ) = 𝑁 )
9		riotaex	⊢ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ V
10		sbceq1g	⊢ ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ V → ( [ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ] ( 2o +o 𝑜 ) = 𝑁 ↔ ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ ( 2o +o 𝑜 ) = 𝑁 ) )
11	9 10	ax-mp	⊢ ( [ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ] ( 2o +o 𝑜 ) = 𝑁 ↔ ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ ( 2o +o 𝑜 ) = 𝑁 )
12		csbov2g	⊢ ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ V → ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ ( 2o +o 𝑜 ) = ( 2o +o ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ 𝑜 ) )
13	9 12	ax-mp	⊢ ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ ( 2o +o 𝑜 ) = ( 2o +o ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ 𝑜 )
14	9	csbvargi	⊢ ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ 𝑜 = ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 )
15	14	oveq2i	⊢ ( 2o +o ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ 𝑜 ) = ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) )
16	13 15	eqtri	⊢ ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ ( 2o +o 𝑜 ) = ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) )
17	16	eqeq1i	⊢ ( ⦋ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ⦌ ( 2o +o 𝑜 ) = 𝑁 ↔ ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) = 𝑁 )
18	11 17	bitri	⊢ ( [ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) / 𝑜 ] ( 2o +o 𝑜 ) = 𝑁 ↔ ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) = 𝑁 )
19	8 18	sylib	⊢ ( ( 𝑁 ∈ On ∧ 2o ⊆ 𝑁 ) → ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) = 𝑁 )
20	3 19	sylan	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) = 𝑁 )
21		simpl	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → 𝑁 ∈ ω )
22	20 21	eqeltrd	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω )
23		riotacl	⊢ ( ∃! 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 → ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ On )
24		riotaund	⊢ ( ¬ ∃! 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 → ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) = ∅ )
25		0elon	⊢ ∅ ∈ On
26	24 25	eqeltrdi	⊢ ( ¬ ∃! 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 → ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ On )
27	23 26	pm2.61i	⊢ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ On
28		nnarcl	⊢ ( ( 2o ∈ On ∧ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ On ) → ( ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω ↔ ( 2o ∈ ω ∧ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ) ) )
29	4 28	mpan	⊢ ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ On → ( ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω ↔ ( 2o ∈ ω ∧ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ) ) )
30	2	biantrur	⊢ ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ↔ ( 2o ∈ ω ∧ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ) )
31	29 30	bitr4di	⊢ ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ On → ( ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω ↔ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ) )
32	27 31	ax-mp	⊢ ( ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω ↔ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω )
33	22 32	sylib	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω )
34		nnacom	⊢ ( ( 2o ∈ ω ∧ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ) → ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) = ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 2o ) )
35	2 33 34	sylancr	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) = ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 2o ) )
36		df-2o	⊢ 2o = suc 1o
37	36	oveq2i	⊢ ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 2o ) = ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o suc 1o )
38		1onn	⊢ 1o ∈ ω
39		nnasuc	⊢ ( ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ∧ 1o ∈ ω ) → ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o suc 1o ) = suc ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) )
40	33 38 39	sylancl	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o suc 1o ) = suc ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) )
41	37 40	syl5eq	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 2o ) = suc ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) )
42	35 20 41	3eqtr3d	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → 𝑁 = suc ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) )
43	3	adantr	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → 𝑁 ∈ On )
44		sucidg	⊢ ( 1o ∈ ω → 1o ∈ suc 1o )
45	38 44	ax-mp	⊢ 1o ∈ suc 1o
46	45 36	eleqtrri	⊢ 1o ∈ 2o
47		ssel	⊢ ( 2o ⊆ 𝑁 → ( 1o ∈ 2o → 1o ∈ 𝑁 ) )
48	46 47	mpi	⊢ ( 2o ⊆ 𝑁 → 1o ∈ 𝑁 )
49	48	ne0d	⊢ ( 2o ⊆ 𝑁 → 𝑁 ≠ ∅ )
50	49	adantl	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → 𝑁 ≠ ∅ )
51		nnlim	⊢ ( 𝑁 ∈ ω → ¬ Lim 𝑁 )
52	51	adantr	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ¬ Lim 𝑁 )
53		onsucuni3	⊢ ( ( 𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁 ) → 𝑁 = suc ∪ 𝑁 )
54	43 50 52 53	syl3anc	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → 𝑁 = suc ∪ 𝑁 )
55		nnacom	⊢ ( ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ∧ 1o ∈ ω ) → ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) = ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) )
56	33 38 55	sylancl	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) = ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) )
57		suceq	⊢ ( ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) = ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) → suc ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) = suc ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) )
58	56 57	syl	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → suc ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) +o 1o ) = suc ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) )
59	42 54 58	3eqtr3d	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → suc ∪ 𝑁 = suc ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) )
60		ordom	⊢ Ord ω
61		ordelss	⊢ ( ( Ord ω ∧ 𝑁 ∈ ω ) → 𝑁 ⊆ ω )
62	60 61	mpan	⊢ ( 𝑁 ∈ ω → 𝑁 ⊆ ω )
63		nnfi	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ Fin )
64		nnunifi	⊢ ( ( 𝑁 ⊆ ω ∧ 𝑁 ∈ Fin ) → ∪ 𝑁 ∈ ω )
65	62 63 64	syl2anc	⊢ ( 𝑁 ∈ ω → ∪ 𝑁 ∈ ω )
66	65	adantr	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ∪ 𝑁 ∈ ω )
67		nnacl	⊢ ( ( 1o ∈ ω ∧ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ) → ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω )
68	38 33 67	sylancr	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω )
69		peano4	⊢ ( ( ∪ 𝑁 ∈ ω ∧ ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ∈ ω ) → ( suc ∪ 𝑁 = suc ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ↔ ∪ 𝑁 = ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) )
70	66 68 69	syl2anc	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( suc ∪ 𝑁 = suc ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ↔ ∪ 𝑁 = ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) )
71	59 70	mpbid	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ∪ 𝑁 = ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) )
72	71	fveq2d	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∪ 𝑁 ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) )
73	72	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∪ 𝑁 ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) )
74	33	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω )
75		df-1o	⊢ 1o = suc ∅
76	75	fveq2i	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 1o ) = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ suc ∅ )
77		rdgsuc	⊢ ( ∅ ∈ On → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ suc ∅ ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∅ ) ) )
78	25 77	ax-mp	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ suc ∅ ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∅ ) )
79		opex	⊢ ⟨ 𝑁 , 𝑦 ⟩ ∈ V
80	79	rdg0	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∅ ) = ⟨ 𝑁 , 𝑦 ⟩
81	80	fveq2i	⊢ ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∅ ) ) = ( 𝐹 ‘ ⟨ 𝑁 , 𝑦 ⟩ )
82	76 78 81	3eqtri	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 1o ) = ( 𝐹 ‘ ⟨ 𝑁 , 𝑦 ⟩ )
83	1	finxpreclem3	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ = ( 𝐹 ‘ ⟨ 𝑁 , 𝑦 ⟩ ) )
84	82 83	eqtr4id	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 1o ) = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ )
85	84	fveq2d	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 1o ) ) = ( 𝐹 ‘ ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) )
86		2on0	⊢ 2o ≠ ∅
87		nnlim	⊢ ( 2o ∈ ω → ¬ Lim 2o )
88	2 87	ax-mp	⊢ ¬ Lim 2o
89		rdgsucuni	⊢ ( ( 2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 2o ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∪ 2o ) ) )
90	4 86 88 89	mp3an	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 2o ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∪ 2o ) )
91		1oequni2o	⊢ 1o = ∪ 2o
92	91	fveq2i	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 1o ) = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∪ 2o )
93	92	fveq2i	⊢ ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 1o ) ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ∪ 2o ) )
94	90 93	eqtr4i	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 2o ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 1o ) )
95	75	fveq2i	⊢ ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ 1o ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ suc ∅ )
96		rdgsuc	⊢ ( ∅ ∈ On → ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ suc ∅ ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∅ ) ) )
97	25 96	ax-mp	⊢ ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ suc ∅ ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∅ ) )
98		opex	⊢ ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ∈ V
99	98	rdg0	⊢ ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∅ ) = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩
100	99	fveq2i	⊢ ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∅ ) ) = ( 𝐹 ‘ ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ )
101	95 97 100	3eqtri	⊢ ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ 1o ) = ( 𝐹 ‘ ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ )
102	85 94 101	3eqtr4g	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 2o ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ 1o ) )
103		1on	⊢ 1o ∈ On
104		rdgeqoa	⊢ ( ( 2o ∈ On ∧ 1o ∈ On ∧ ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω ) → ( ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 2o ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ 1o ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) ) )
105	4 103 104	mp3an12	⊢ ( ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ∈ ω → ( ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 2o ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ 1o ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) ) )
106	74 102 105	sylc	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ( 1o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) )
107	20	fveq2d	⊢ ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) )
108	107	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ( 2o +o ( ℩ 𝑜 ∈ On ( 2o +o 𝑜 ) = 𝑁 ) ) ) = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) )
109	73 106 108	3eqtr2rd	⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑦 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) = ( rec ( 𝐹 , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑦 ) ⟩ ) ‘ ∪ 𝑁 ) )