Theorem finxpreclem4 38149

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

Hypothesis

Ref	Expression
finxpreclem4.1	⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))

Assertion

Ref	Expression
finxpreclem4	⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁))

Distinct variable groups:   𝑛,𝑁,𝑥   𝑈,𝑛,𝑥   𝑦,𝑛,𝑥

Allowed substitution hints:   𝑈(𝑦)   𝐹(𝑥, 𝑦, 𝑛)   𝑁(𝑦)

Proof of Theorem finxpreclem4

Dummy variable 𝑜 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2onn 8631	. . . . . . . 8 ⊢ 2o ∈ ω
2		nnon 7869	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → 𝑁 ∈ On)
3		2on 8470	. . . . . . . . . . . . . 14 ⊢ 2o ∈ On
4		oawordeu 8543	. . . . . . . . . . . . . 14 ⊢ (((2o ∈ On ∧ 𝑁 ∈ On) ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
5	3, 4	mpanl1 713	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
6		riotasbc 7389	. . . . . . . . . . . . 13 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
7	5, 6	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
8		riotaex 7375	. . . . . . . . . . . . . 14 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V
9		sbceq1g 4375	. . . . . . . . . . . . . 14 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V → ([(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = 𝑁))
10	8, 9	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = 𝑁)
11		csbov2g 7462	. . . . . . . . . . . . . . . 16 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V → ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = (2o +o ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜))
12	8, 11	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = (2o +o ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜)
13	8	csbvargi 4393	. . . . . . . . . . . . . . . 16 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜 = (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)
14	13	oveq2i 7425	. . . . . . . . . . . . . . 15 ⊢ (2o +o ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
15	12, 14	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
16	15	eqeq1i 2765	. . . . . . . . . . . . 13 ⊢ (⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
17	10, 16	bitri 278	. . . . . . . . . . . 12 ⊢ ([(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
18	7, 17	sylib 221	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
19	2, 18	sylan 592	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
20		simpl 488	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ ω)
21	19, 20	eqeltrd 2860	. . . . . . . . 9 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
22		riotacl 7388	. . . . . . . . . . 11 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
23		riotaund 7410	. . . . . . . . . . . 12 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) = ∅)
24		0elon 6413	. . . . . . . . . . . 12 ⊢ ∅ ∈ On
25	23, 24	eqeltrdi 2868	. . . . . . . . . . 11 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
26	22, 25	pm2.61i 184	. . . . . . . . . 10 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On
27		nnarcl 8605	. . . . . . . . . . . 12 ⊢ ((2o ∈ On ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On) → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
28	3, 27	mpan 703	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
29	1	biantrur 540	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
30	28, 29	bitr4di 292	. . . . . . . . . 10 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
31	26, 30	ax-mp 5	. . . . . . . . 9 ⊢ ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
32	21, 31	sylib 221	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
33		nnacom 8606	. . . . . . . 8 ⊢ ((2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
34	1, 32, 33	sylancr 599	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
35		df-2o 8457	. . . . . . . . 9 ⊢ 2o = suc 1o
36	35	oveq2i 7425	. . . . . . . 8 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o)
37		1onn 8629	. . . . . . . . 9 ⊢ 1o ∈ ω
38		nnasuc 8595	. . . . . . . . 9 ⊢ (((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
39	32, 37, 38	sylancl 598	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
40	36, 39	eqtrid 2807	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
41	34, 19, 40	3eqtr3d 2803	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
42	2	adantr 486	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ On)
43		sucidg 6441	. . . . . . . . . . . 12 ⊢ (1o ∈ ω → 1o ∈ suc 1o)
44	37, 43	ax-mp 5	. . . . . . . . . . 11 ⊢ 1o ∈ suc 1o
45	44, 35	eleqtrri 2859	. . . . . . . . . 10 ⊢ 1o ∈ 2o
46		ssel 3925	. . . . . . . . . 10 ⊢ (2o ⊆ 𝑁 → (1o ∈ 2o → 1o ∈ 𝑁))
47	45, 46	mpi 21	. . . . . . . . 9 ⊢ (2o ⊆ 𝑁 → 1o ∈ 𝑁)
48	47	ne0d 4288	. . . . . . . 8 ⊢ (2o ⊆ 𝑁 → 𝑁 ≠ ∅)
49	48	adantl 487	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ≠ ∅)
50		nnlim 7877	. . . . . . . 8 ⊢ (𝑁 ∈ ω → ¬ Lim 𝑁)
51	50	adantr 486	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ¬ Lim 𝑁)
52		onsucuni3 38122	. . . . . . 7 ⊢ ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁) → 𝑁 = suc ∪ 𝑁)
53	42, 49, 51, 52	syl3anc 1398	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ∪ 𝑁)
54		nnacom 8606	. . . . . . . 8 ⊢ (((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
55	32, 37, 54	sylancl 598	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
56		suceq 6426	. . . . . . 7 ⊢ (((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) → suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
57	55, 56	syl 18	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
58	41, 53, 57	3eqtr3d 2803	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
59		ordom 7873	. . . . . . . . 9 ⊢ Ord ω
60		ordelss 6373	. . . . . . . . 9 ⊢ ((Ord ω ∧ 𝑁 ∈ ω) → 𝑁 ⊆ ω)
61	59, 60	mpan 703	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ⊆ ω)
62		nnfi 9163	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ∈ Fin)
63		nnunifi 9262	. . . . . . . 8 ⊢ ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → ∪ 𝑁 ∈ ω)
64	61, 62, 63	syl2anc 596	. . . . . . 7 ⊢ (𝑁 ∈ ω → ∪ 𝑁 ∈ ω)
65	64	adantr 486	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 ∈ ω)
66		nnacl 8600	. . . . . . 7 ⊢ ((1o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
67	37, 32, 66	sylancr 599	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
68		peano4 7890	. . . . . 6 ⊢ ((∪ 𝑁 ∈ ω ∧ (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω) → (suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
69	65, 67, 68	syl2anc 596	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
70	58, 69	mpbid 235	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
71	70	fveq2d 6883	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
72	71	adantr 486	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
73	32	adantr 486	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
74		df-1o 8456	. . . . . . . 8 ⊢ 1o = suc ∅
75	74	fveq2i 6882	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅)
76		rdgsuc 8414	. . . . . . . 8 ⊢ (∅ ∈ On → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)))
77	24, 76	ax-mp 5	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅))
78		opex 5439	. . . . . . . . 9 ⊢ ⟨𝑁, 𝑦⟩ ∈ V
79	78	rdg0 8411	. . . . . . . 8 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅) = ⟨𝑁, 𝑦⟩
80	79	fveq2i 6882	. . . . . . 7 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)) = (𝐹‘⟨𝑁, 𝑦⟩)
81	75, 77, 80	3eqtri 2787	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (𝐹‘⟨𝑁, 𝑦⟩)
82		finxpreclem4.1	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
83	82	finxpreclem3 38148	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ⟨∪ 𝑁, (1st ‘𝑦)⟩ = (𝐹‘⟨𝑁, 𝑦⟩))
84	81, 83	eqtr4id 2814	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = ⟨∪ 𝑁, (1st ‘𝑦)⟩)
85	84	fveq2d 6883	. . . 4 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩))
86		2on0 8471	. . . . . 6 ⊢ 2o ≠ ∅
87		nnlim 7877	. . . . . . 7 ⊢ (2o ∈ ω → ¬ Lim 2o)
88	1, 87	ax-mp 5	. . . . . 6 ⊢ ¬ Lim 2o
89		rdgsucuni 38124	. . . . . 6 ⊢ ((2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)))
90	3, 86, 88, 89	mp3an 1490	. . . . 5 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
91		1oequni2o 38123	. . . . . . 7 ⊢ 1o = ∪ 2o
92	91	fveq2i 6882	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)
93	92	fveq2i 6882	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
94	90, 93	eqtr4i 2786	. . . 4 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o))
95	74	fveq2i 6882	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅)
96		rdgsuc 8414	. . . . . 6 ⊢ (∅ ∈ On → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)))
97	24, 96	ax-mp 5	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅))
98		opex 5439	. . . . . . 7 ⊢ ⟨∪ 𝑁, (1st ‘𝑦)⟩ ∈ V
99	98	rdg0 8411	. . . . . 6 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅) = ⟨∪ 𝑁, (1st ‘𝑦)⟩
100	99	fveq2i 6882	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
101	95, 97, 100	3eqtri 2787	. . . 4 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
102	85, 94, 101	3eqtr4g 2820	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o))
103		1on 8469	. . . 4 ⊢ 1o ∈ On
104		rdgeqoa 38125	. . . 4 ⊢ ((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	3, 103, 104	mp3an12 1480	. . 3 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω → ((rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))))
106	73, 102, 105	sylc 66	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
107	19	fveq2d 6883	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
108	107	adantr 486	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
109	72, 106, 108	3eqtr2rd 2802	1 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∃!wreu 3363  Vcvv 3450  [wsbc 3739  ⦋csb 3847   ⊆ wss 3899  ∅c0 4279  ifcif 4482  ⟨cop 4590  ∪ cuni 4867   × cxp 5653  Ord word 6356  Oncon0 6357  Lim wlim 6358  suc csuc 6359  ‘cfv 6533  ℩crio 7370  (class class class)co 7414   ∈ cmpo 7416  ωcom 7863  1^st c1st 7985  reccrdg 8399  1_oc1o 8449  2_oc2o 8450   +_o coa 8453  Fincfn 8953

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8456  df-2o 8457  df-oadd 8460  df-en 8954  df-fin 8957

This theorem is used by:  finxpsuclem  38152