Theorem finxpreclem4 37538

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 8568	. . . . . . . 8 ⊢ 2o ∈ ω
2		nnon 7812	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → 𝑁 ∈ On)
3		2on 8408	. . . . . . . . . . . . . 14 ⊢ 2o ∈ On
4		oawordeu 8480	. . . . . . . . . . . . . 14 ⊢ (((2o ∈ On ∧ 𝑁 ∈ On) ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
5	3, 4	mpanl1 700	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
6		riotasbc 7331	. . . . . . . . . . . . 13 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
7	5, 6	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
8		riotaex 7317	. . . . . . . . . . . . . 14 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V
9		sbceq1g 4367	. . . . . . . . . . . . . 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 7404	. . . . . . . . . . . . . . . 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 4385	. . . . . . . . . . . . . . . 16 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜 = (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)
14	13	oveq2i 7367	. . . . . . . . . . . . . . 15 ⊢ (2o +o ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
15	12, 14	eqtri 2757	. . . . . . . . . . . . . 14 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
16	15	eqeq1i 2739	. . . . . . . . . . . . 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 7330	. . . . . . . . . . 11 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
23		riotaund 7352	. . . . . . . . . . . 12 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) = ∅)
24		0elon 6370	. . . . . . . . . . . 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 8542	. . . . . . . . . . . 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 8543	. . . . . . . 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 8396	. . . . . . . . 9 ⊢ 2o = suc 1o
36	35	oveq2i 7367	. . . . . . . 8 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o)
37		1onn 8566	. . . . . . . . 9 ⊢ 1o ∈ ω
38		nnasuc 8532	. . . . . . . . 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 2781	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
41	34, 19, 40	3eqtr3d 2777	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
42	2	adantr 480	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ On)
43		sucidg 6398	. . . . . . . . . . . 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 3925	. . . . . . . . . 10 ⊢ (2o ⊆ 𝑁 → (1o ∈ 2o → 1o ∈ 𝑁))
47	45, 46	mpi 20	. . . . . . . . 9 ⊢ (2o ⊆ 𝑁 → 1o ∈ 𝑁)
48	47	ne0d 4292	. . . . . . . 8 ⊢ (2o ⊆ 𝑁 → 𝑁 ≠ ∅)
49	48	adantl 481	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ≠ ∅)
50		nnlim 7820	. . . . . . . 8 ⊢ (𝑁 ∈ ω → ¬ Lim 𝑁)
51	50	adantr 480	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ¬ Lim 𝑁)
52		onsucuni3 37511	. . . . . . 7 ⊢ ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁) → 𝑁 = suc ∪ 𝑁)
53	42, 49, 51, 52	syl3anc 1373	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ∪ 𝑁)
54		nnacom 8543	. . . . . . . 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 6383	. . . . . . 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 2777	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
59		ordom 7816	. . . . . . . . 9 ⊢ Ord ω
60		ordelss 6331	. . . . . . . . 9 ⊢ ((Ord ω ∧ 𝑁 ∈ ω) → 𝑁 ⊆ ω)
61	59, 60	mpan 690	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ⊆ ω)
62		nnfi 9090	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ∈ Fin)
63		nnunifi 9189	. . . . . . . 8 ⊢ ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → ∪ 𝑁 ∈ ω)
64	61, 62, 63	syl2anc 584	. . . . . . 7 ⊢ (𝑁 ∈ ω → ∪ 𝑁 ∈ ω)
65	64	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 ∈ ω)
66		nnacl 8537	. . . . . . 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 7832	. . . . . 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 6836	. . 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 8395	. . . . . . . 8 ⊢ 1o = suc ∅
75	74	fveq2i 6835	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅)
76		rdgsuc 8353	. . . . . . . 8 ⊢ (∅ ∈ On → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)))
77	24, 76	ax-mp 5	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅))
78		opex 5410	. . . . . . . . 9 ⊢ ⟨𝑁, 𝑦⟩ ∈ V
79	78	rdg0 8350	. . . . . . . 8 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅) = ⟨𝑁, 𝑦⟩
80	79	fveq2i 6835	. . . . . . 7 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)) = (𝐹‘⟨𝑁, 𝑦⟩)
81	75, 77, 80	3eqtri 2761	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (𝐹‘⟨𝑁, 𝑦⟩)
82		finxpreclem4.1	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
83	82	finxpreclem3 37537	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ⟨∪ 𝑁, (1st ‘𝑦)⟩ = (𝐹‘⟨𝑁, 𝑦⟩))
84	81, 83	eqtr4id 2788	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = ⟨∪ 𝑁, (1st ‘𝑦)⟩)
85	84	fveq2d 6836	. . . 4 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩))
86		2on0 8409	. . . . . 6 ⊢ 2o ≠ ∅
87		nnlim 7820	. . . . . . 7 ⊢ (2o ∈ ω → ¬ Lim 2o)
88	1, 87	ax-mp 5	. . . . . 6 ⊢ ¬ Lim 2o
89		rdgsucuni 37513	. . . . . 6 ⊢ ((2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)))
90	3, 86, 88, 89	mp3an 1463	. . . . 5 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
91		1oequni2o 37512	. . . . . . 7 ⊢ 1o = ∪ 2o
92	91	fveq2i 6835	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)
93	92	fveq2i 6835	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
94	90, 93	eqtr4i 2760	. . . 4 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o))
95	74	fveq2i 6835	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅)
96		rdgsuc 8353	. . . . . 6 ⊢ (∅ ∈ On → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)))
97	24, 96	ax-mp 5	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅))
98		opex 5410	. . . . . . 7 ⊢ ⟨∪ 𝑁, (1st ‘𝑦)⟩ ∈ V
99	98	rdg0 8350	. . . . . 6 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅) = ⟨∪ 𝑁, (1st ‘𝑦)⟩
100	99	fveq2i 6835	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
101	95, 97, 100	3eqtri 2761	. . . 4 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
102	85, 94, 101	3eqtr4g 2794	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o))
103		1on 8407	. . . 4 ⊢ 1o ∈ On
104		rdgeqoa 37514	. . . 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 6836	. . 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 2776	1 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ∃!wreu 3346  Vcvv 3438  [wsbc 3738  ⦋csb 3847   ⊆ wss 3899  ∅c0 4283  ifcif 4477  ⟨cop 4584  ∪ cuni 4861   × cxp 5620  Ord word 6314  Oncon0 6315  Lim wlim 6316  suc csuc 6317  ‘cfv 6490  ℩crio 7312  (class class class)co 7356   ∈ cmpo 7358  ωcom 7806  1^st c1st 7929  reccrdg 8338  1_oc1o 8388  2_oc2o 8389   +_o coa 8392  Fincfn 8881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-oadd 8399  df-en 8882  df-fin 8885

This theorem is referenced by:  finxpsuclem  37541