Theorem finxpreclem4 37412

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 8654	. . . . . . . 8 ⊢ 2o ∈ ω
2		nnon 7867	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → 𝑁 ∈ On)
3		2on 8494	. . . . . . . . . . . . . 14 ⊢ 2o ∈ On
4		oawordeu 8567	. . . . . . . . . . . . . 14 ⊢ (((2o ∈ On ∧ 𝑁 ∈ On) ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
5	3, 4	mpanl1 700	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
6		riotasbc 7380	. . . . . . . . . . . . 13 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
7	5, 6	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
8		riotaex 7366	. . . . . . . . . . . . . 14 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V
9		sbceq1g 4392	. . . . . . . . . . . . . 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 7453	. . . . . . . . . . . . . . . 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 4410	. . . . . . . . . . . . . . . 16 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜 = (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)
14	13	oveq2i 7416	. . . . . . . . . . . . . . 15 ⊢ (2o +o ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
15	12, 14	eqtri 2758	. . . . . . . . . . . . . 14 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
16	15	eqeq1i 2740	. . . . . . . . . . . . 13 ⊢ (⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
17	10, 16	bitri 275	. . . . . . . . . . . 12 ⊢ ([(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
18	7, 17	sylib 218	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
19	2, 18	sylan 580	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
20		simpl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ ω)
21	19, 20	eqeltrd 2834	. . . . . . . . 9 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
22		riotacl 7379	. . . . . . . . . . 11 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
23		riotaund 7401	. . . . . . . . . . . 12 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) = ∅)
24		0elon 6407	. . . . . . . . . . . 12 ⊢ ∅ ∈ On
25	23, 24	eqeltrdi 2842	. . . . . . . . . . 11 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
26	22, 25	pm2.61i 182	. . . . . . . . . 10 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On
27		nnarcl 8628	. . . . . . . . . . . 12 ⊢ ((2o ∈ On ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On) → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
28	3, 27	mpan 690	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
29	1	biantrur 530	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
30	28, 29	bitr4di 289	. . . . . . . . . 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 218	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
33		nnacom 8629	. . . . . . . 8 ⊢ ((2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
34	1, 32, 33	sylancr 587	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
35		df-2o 8481	. . . . . . . . 9 ⊢ 2o = suc 1o
36	35	oveq2i 7416	. . . . . . . 8 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o)
37		1onn 8652	. . . . . . . . 9 ⊢ 1o ∈ ω
38		nnasuc 8618	. . . . . . . . 9 ⊢ (((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
39	32, 37, 38	sylancl 586	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
40	36, 39	eqtrid 2782	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
41	34, 19, 40	3eqtr3d 2778	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
42	2	adantr 480	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ On)
43		sucidg 6435	. . . . . . . . . . . 12 ⊢ (1o ∈ ω → 1o ∈ suc 1o)
44	37, 43	ax-mp 5	. . . . . . . . . . 11 ⊢ 1o ∈ suc 1o
45	44, 35	eleqtrri 2833	. . . . . . . . . 10 ⊢ 1o ∈ 2o
46		ssel 3952	. . . . . . . . . 10 ⊢ (2o ⊆ 𝑁 → (1o ∈ 2o → 1o ∈ 𝑁))
47	45, 46	mpi 20	. . . . . . . . 9 ⊢ (2o ⊆ 𝑁 → 1o ∈ 𝑁)
48	47	ne0d 4317	. . . . . . . 8 ⊢ (2o ⊆ 𝑁 → 𝑁 ≠ ∅)
49	48	adantl 481	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ≠ ∅)
50		nnlim 7875	. . . . . . . 8 ⊢ (𝑁 ∈ ω → ¬ Lim 𝑁)
51	50	adantr 480	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ¬ Lim 𝑁)
52		onsucuni3 37385	. . . . . . 7 ⊢ ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁) → 𝑁 = suc ∪ 𝑁)
53	42, 49, 51, 52	syl3anc 1373	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ∪ 𝑁)
54		nnacom 8629	. . . . . . . 8 ⊢ (((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
55	32, 37, 54	sylancl 586	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
56		suceq 6419	. . . . . . 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 17	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
58	41, 53, 57	3eqtr3d 2778	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
59		ordom 7871	. . . . . . . . 9 ⊢ Ord ω
60		ordelss 6368	. . . . . . . . 9 ⊢ ((Ord ω ∧ 𝑁 ∈ ω) → 𝑁 ⊆ ω)
61	59, 60	mpan 690	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ⊆ ω)
62		nnfi 9181	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ∈ Fin)
63		nnunifi 9299	. . . . . . . 8 ⊢ ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → ∪ 𝑁 ∈ ω)
64	61, 62, 63	syl2anc 584	. . . . . . 7 ⊢ (𝑁 ∈ ω → ∪ 𝑁 ∈ ω)
65	64	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 ∈ ω)
66		nnacl 8623	. . . . . . 7 ⊢ ((1o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
67	37, 32, 66	sylancr 587	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
68		peano4 7888	. . . . . 6 ⊢ ((∪ 𝑁 ∈ ω ∧ (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω) → (suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
69	65, 67, 68	syl2anc 584	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
70	58, 69	mpbid 232	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
71	70	fveq2d 6880	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
72	71	adantr 480	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
73	32	adantr 480	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
74		df-1o 8480	. . . . . . . 8 ⊢ 1o = suc ∅
75	74	fveq2i 6879	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅)
76		rdgsuc 8438	. . . . . . . 8 ⊢ (∅ ∈ On → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)))
77	24, 76	ax-mp 5	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅))
78		opex 5439	. . . . . . . . 9 ⊢ ⟨𝑁, 𝑦⟩ ∈ V
79	78	rdg0 8435	. . . . . . . 8 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅) = ⟨𝑁, 𝑦⟩
80	79	fveq2i 6879	. . . . . . 7 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)) = (𝐹‘⟨𝑁, 𝑦⟩)
81	75, 77, 80	3eqtri 2762	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (𝐹‘⟨𝑁, 𝑦⟩)
82		finxpreclem4.1	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
83	82	finxpreclem3 37411	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ⟨∪ 𝑁, (1st ‘𝑦)⟩ = (𝐹‘⟨𝑁, 𝑦⟩))
84	81, 83	eqtr4id 2789	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = ⟨∪ 𝑁, (1st ‘𝑦)⟩)
85	84	fveq2d 6880	. . . 4 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩))
86		2on0 8496	. . . . . 6 ⊢ 2o ≠ ∅
87		nnlim 7875	. . . . . . 7 ⊢ (2o ∈ ω → ¬ Lim 2o)
88	1, 87	ax-mp 5	. . . . . 6 ⊢ ¬ Lim 2o
89		rdgsucuni 37387	. . . . . 6 ⊢ ((2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)))
90	3, 86, 88, 89	mp3an 1463	. . . . 5 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
91		1oequni2o 37386	. . . . . . 7 ⊢ 1o = ∪ 2o
92	91	fveq2i 6879	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)
93	92	fveq2i 6879	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
94	90, 93	eqtr4i 2761	. . . 4 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o))
95	74	fveq2i 6879	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅)
96		rdgsuc 8438	. . . . . 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 8435	. . . . . 6 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅) = ⟨∪ 𝑁, (1st ‘𝑦)⟩
100	99	fveq2i 6879	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
101	95, 97, 100	3eqtri 2762	. . . 4 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
102	85, 94, 101	3eqtr4g 2795	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o))
103		1on 8492	. . . 4 ⊢ 1o ∈ On
104		rdgeqoa 37388	. . . 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 1453	. . 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 65	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
107	19	fveq2d 6880	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
108	107	adantr 480	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
109	72, 106, 108	3eqtr2rd 2777	1 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ∃!wreu 3357  Vcvv 3459  [wsbc 3765  ⦋csb 3874   ⊆ wss 3926  ∅c0 4308  ifcif 4500  ⟨cop 4607  ∪ cuni 4883   × cxp 5652  Ord word 6351  Oncon0 6352  Lim wlim 6353  suc csuc 6354  ‘cfv 6531  ℩crio 7361  (class class class)co 7405   ∈ cmpo 7407  ωcom 7861  1^st c1st 7986  reccrdg 8423  1_oc1o 8473  2_oc2o 8474   +_o coa 8477  Fincfn 8959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-en 8960  df-fin 8963

This theorem is referenced by:  finxpsuclem  37415