Theorem finxpreclem4 34206

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 8116	. . . . . . . 8 ⊢ 2o ∈ ω
2		nnon 7442	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → 𝑁 ∈ On)
3		2on 7962	. . . . . . . . . . . . . 14 ⊢ 2o ∈ On
4		oawordeu 8031	. . . . . . . . . . . . . 14 ⊢ (((2o ∈ On ∧ 𝑁 ∈ On) ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
5	3, 4	mpanl1 696	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
6		riotasbc 6992	. . . . . . . . . . . . 13 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
7	5, 6	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
8		riotaex 6981	. . . . . . . . . . . . . 14 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V
9		sbceq1g 4286	. . . . . . . . . . . . . 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 7061	. . . . . . . . . . . . . . . 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 4299	. . . . . . . . . . . . . . . 16 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜 = (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)
14	13	oveq2i 7027	. . . . . . . . . . . . . . 15 ⊢ (2o +o ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
15	12, 14	eqtri 2819	. . . . . . . . . . . . . 14 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
16	15	eqeq1i 2800	. . . . . . . . . . . . 13 ⊢ (⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
17	10, 16	bitri 276	. . . . . . . . . . . 12 ⊢ ([(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
18	7, 17	sylib 219	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
19	2, 18	sylan 580	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
20		simpl 483	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ ω)
21	19, 20	eqeltrd 2883	. . . . . . . . 9 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
22		riotacl 6991	. . . . . . . . . . 11 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
23		riotaund 7013	. . . . . . . . . . . 12 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) = ∅)
24		0elon 6119	. . . . . . . . . . . 12 ⊢ ∅ ∈ On
25	23, 24	syl6eqel 2891	. . . . . . . . . . 11 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
26	22, 25	pm2.61i 183	. . . . . . . . . 10 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On
27		nnarcl 8092	. . . . . . . . . . . 12 ⊢ ((2o ∈ On ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On) → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
28	3, 27	mpan 686	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
29	1	biantrur 531	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
30	28, 29	syl6bbr 290	. . . . . . . . . 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 219	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
33		nnacom 8093	. . . . . . . 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 7954	. . . . . . . . 9 ⊢ 2o = suc 1o
36	35	oveq2i 7027	. . . . . . . 8 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o)
37		1onn 8115	. . . . . . . . 9 ⊢ 1o ∈ ω
38		nnasuc 8082	. . . . . . . . 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	syl5eq 2843	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
41	34, 19, 40	3eqtr3d 2839	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
42	2	adantr 481	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ On)
43		sucidg 6144	. . . . . . . . . . . 12 ⊢ (1o ∈ ω → 1o ∈ suc 1o)
44	37, 43	ax-mp 5	. . . . . . . . . . 11 ⊢ 1o ∈ suc 1o
45	44, 35	eleqtrri 2882	. . . . . . . . . 10 ⊢ 1o ∈ 2o
46		ssel 3883	. . . . . . . . . 10 ⊢ (2o ⊆ 𝑁 → (1o ∈ 2o → 1o ∈ 𝑁))
47	45, 46	mpi 20	. . . . . . . . 9 ⊢ (2o ⊆ 𝑁 → 1o ∈ 𝑁)
48	47	ne0d 4221	. . . . . . . 8 ⊢ (2o ⊆ 𝑁 → 𝑁 ≠ ∅)
49	48	adantl 482	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ≠ ∅)
50		nnlim 7449	. . . . . . . 8 ⊢ (𝑁 ∈ ω → ¬ Lim 𝑁)
51	50	adantr 481	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ¬ Lim 𝑁)
52		onsucuni3 34179	. . . . . . 7 ⊢ ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁) → 𝑁 = suc ∪ 𝑁)
53	42, 49, 51, 52	syl3anc 1364	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ∪ 𝑁)
54		nnacom 8093	. . . . . . . 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 6131	. . . . . . 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 2839	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
59		ordom 7445	. . . . . . . . 9 ⊢ Ord ω
60		ordelss 6082	. . . . . . . . 9 ⊢ ((Ord ω ∧ 𝑁 ∈ ω) → 𝑁 ⊆ ω)
61	59, 60	mpan 686	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ⊆ ω)
62		nnfi 8557	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ∈ Fin)
63		nnunifi 8615	. . . . . . . 8 ⊢ ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → ∪ 𝑁 ∈ ω)
64	61, 62, 63	syl2anc 584	. . . . . . 7 ⊢ (𝑁 ∈ ω → ∪ 𝑁 ∈ ω)
65	64	adantr 481	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 ∈ ω)
66		nnacl 8087	. . . . . . 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 7460	. . . . . 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 233	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
71	70	fveq2d 6542	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
72	71	adantr 481	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
73	32	adantr 481	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
74		finxpreclem4.1	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
75	74	finxpreclem3 34205	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ⟨∪ 𝑁, (1st ‘𝑦)⟩ = (𝐹‘⟨𝑁, 𝑦⟩))
76		df-1o 7953	. . . . . . . 8 ⊢ 1o = suc ∅
77	76	fveq2i 6541	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅)
78		rdgsuc 7912	. . . . . . . 8 ⊢ (∅ ∈ On → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)))
79	24, 78	ax-mp 5	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅))
80		opex 5248	. . . . . . . . 9 ⊢ ⟨𝑁, 𝑦⟩ ∈ V
81	80	rdg0 7909	. . . . . . . 8 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅) = ⟨𝑁, 𝑦⟩
82	81	fveq2i 6541	. . . . . . 7 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)) = (𝐹‘⟨𝑁, 𝑦⟩)
83	77, 79, 82	3eqtri 2823	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (𝐹‘⟨𝑁, 𝑦⟩)
84	75, 83	syl6reqr 2850	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = ⟨∪ 𝑁, (1st ‘𝑦)⟩)
85	84	fveq2d 6542	. . . 4 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩))
86		2on0 7964	. . . . . 6 ⊢ 2o ≠ ∅
87		nnlim 7449	. . . . . . 7 ⊢ (2o ∈ ω → ¬ Lim 2o)
88	1, 87	ax-mp 5	. . . . . 6 ⊢ ¬ Lim 2o
89		rdgsucuni 34181	. . . . . 6 ⊢ ((2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)))
90	3, 86, 88, 89	mp3an 1453	. . . . 5 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
91		1oequni2o 34180	. . . . . . 7 ⊢ 1o = ∪ 2o
92	91	fveq2i 6541	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)
93	92	fveq2i 6541	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
94	90, 93	eqtr4i 2822	. . . 4 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o))
95	76	fveq2i 6541	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅)
96		rdgsuc 7912	. . . . . 6 ⊢ (∅ ∈ On → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)))
97	24, 96	ax-mp 5	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅))
98		opex 5248	. . . . . . 7 ⊢ ⟨∪ 𝑁, (1st ‘𝑦)⟩ ∈ V
99	98	rdg0 7909	. . . . . 6 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅) = ⟨∪ 𝑁, (1st ‘𝑦)⟩
100	99	fveq2i 6541	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
101	95, 97, 100	3eqtri 2823	. . . 4 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
102	85, 94, 101	3eqtr4g 2856	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o))
103		1on 7960	. . . 4 ⊢ 1o ∈ On
104		rdgeqoa 34182	. . . 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 1443	. . 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 6542	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
108	107	adantr 481	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
109	72, 106, 108	3eqtr2rd 2838	1 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081   ≠ wne 2984  ∃!wreu 3107  Vcvv 3437  [wsbc 3706  ⦋csb 3811   ⊆ wss 3859  ∅c0 4211  ifcif 4381  ⟨cop 4478  ∪ cuni 4745   × cxp 5441  Ord word 6065  Oncon0 6066  Lim wlim 6067  suc csuc 6068  ‘cfv 6225  ℩crio 6976  (class class class)co 7016   ∈ cmpo 7018  ωcom 7436  1^st c1st 7543  reccrdg 7897  1_oc1o 7946  2_oc2o 7947   +_o coa 7950  Fincfn 8357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-2o 7954  df-oadd 7957  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361

This theorem is referenced by:  finxpsuclem  34209