Theorem finxpreclem4 37888

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 8612	. . . . . . . 8 ⊢ 2o ∈ ω
2		nnon 7852	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → 𝑁 ∈ On)
3		2on 8451	. . . . . . . . . . . . . 14 ⊢ 2o ∈ On
4		oawordeu 8524	. . . . . . . . . . . . . 14 ⊢ (((2o ∈ On ∧ 𝑁 ∈ On) ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
5	3, 4	mpanl1 710	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
6		riotasbc 7371	. . . . . . . . . . . . 13 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
7	5, 6	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → [(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
8		riotaex 7357	. . . . . . . . . . . . . 14 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V
9		sbceq1g 4371	. . . . . . . . . . . . . 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 7444	. . . . . . . . . . . . . . . 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 4389	. . . . . . . . . . . . . . . 16 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜 = (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)
14	13	oveq2i 7407	. . . . . . . . . . . . . . 15 ⊢ (2o +o ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
15	12, 14	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ ⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))
16	15	eqeq1i 2767	. . . . . . . . . . . . 13 ⊢ (⦋(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜⦌(2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
17	10, 16	bitri 277	. . . . . . . . . . . 12 ⊢ ([(℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
18	7, 17	sylib 220	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ On ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
19	2, 18	sylan 589	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
20		simpl 486	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ ω)
21	19, 20	eqeltrd 2862	. . . . . . . . 9 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
22		riotacl 7370	. . . . . . . . . . 11 ⊢ (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
23		riotaund 7392	. . . . . . . . . . . 12 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) = ∅)
24		0elon 6401	. . . . . . . . . . . 12 ⊢ ∅ ∈ On
25	23, 24	eqeltrdi 2870	. . . . . . . . . . 11 ⊢ (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
26	22, 25	pm2.61i 183	. . . . . . . . . 10 ⊢ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On
27		nnarcl 8586	. . . . . . . . . . . 12 ⊢ ((2o ∈ On ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On) → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
28	3, 27	mpan 700	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
29	1	biantrur 538	. . . . . . . . . . 11 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ↔ (2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
30	28, 29	bitr4di 291	. . . . . . . . . 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 220	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
33		nnacom 8587	. . . . . . . 8 ⊢ ((2o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
34	1, 32, 33	sylancr 596	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
35		df-2o 8438	. . . . . . . . 9 ⊢ 2o = suc 1o
36	35	oveq2i 7407	. . . . . . . 8 ⊢ ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o)
37		1onn 8610	. . . . . . . . 9 ⊢ 1o ∈ ω
38		nnasuc 8576	. . . . . . . . 9 ⊢ (((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
39	32, 37, 38	sylancl 595	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
40	36, 39	eqtrid 2809	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
41	34, 19, 40	3eqtr3d 2805	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
42	2	adantr 484	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ∈ On)
43		sucidg 6429	. . . . . . . . . . . 12 ⊢ (1o ∈ ω → 1o ∈ suc 1o)
44	37, 43	ax-mp 5	. . . . . . . . . . 11 ⊢ 1o ∈ suc 1o
45	44, 35	eleqtrri 2861	. . . . . . . . . 10 ⊢ 1o ∈ 2o
46		ssel 3930	. . . . . . . . . 10 ⊢ (2o ⊆ 𝑁 → (1o ∈ 2o → 1o ∈ 𝑁))
47	45, 46	mpi 20	. . . . . . . . 9 ⊢ (2o ⊆ 𝑁 → 1o ∈ 𝑁)
48	47	ne0d 4294	. . . . . . . 8 ⊢ (2o ⊆ 𝑁 → 𝑁 ≠ ∅)
49	48	adantl 485	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 ≠ ∅)
50		nnlim 7860	. . . . . . . 8 ⊢ (𝑁 ∈ ω → ¬ Lim 𝑁)
51	50	adantr 484	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ¬ Lim 𝑁)
52		onsucuni3 37861	. . . . . . 7 ⊢ ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁) → 𝑁 = suc ∪ 𝑁)
53	42, 49, 51, 52	syl3anc 1390	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → 𝑁 = suc ∪ 𝑁)
54		nnacom 8587	. . . . . . . 8 ⊢ (((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
55	32, 37, 54	sylancl 595	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ((℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
56		suceq 6414	. . . . . . 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 2805	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
59		ordom 7856	. . . . . . . . 9 ⊢ Ord ω
60		ordelss 6362	. . . . . . . . 9 ⊢ ((Ord ω ∧ 𝑁 ∈ ω) → 𝑁 ⊆ ω)
61	59, 60	mpan 700	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ⊆ ω)
62		nnfi 9136	. . . . . . . 8 ⊢ (𝑁 ∈ ω → 𝑁 ∈ Fin)
63		nnunifi 9235	. . . . . . . 8 ⊢ ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → ∪ 𝑁 ∈ ω)
64	61, 62, 63	syl2anc 593	. . . . . . 7 ⊢ (𝑁 ∈ ω → ∪ 𝑁 ∈ ω)
65	64	adantr 484	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 ∈ ω)
66		nnacl 8581	. . . . . . 7 ⊢ ((1o ∈ ω ∧ (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
67	37, 32, 66	sylancr 596	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
68		peano4 7873	. . . . . 6 ⊢ ((∪ 𝑁 ∈ ω ∧ (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω) → (suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
69	65, 67, 68	syl2anc 593	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (suc ∪ 𝑁 = suc (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
70	58, 69	mpbid 234	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → ∪ 𝑁 = (1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
71	70	fveq2d 6871	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
72	71	adantr 484	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘(1o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
73	32	adantr 484	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
74		df-1o 8437	. . . . . . . 8 ⊢ 1o = suc ∅
75	74	fveq2i 6870	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅)
76		rdgsuc 8395	. . . . . . . 8 ⊢ (∅ ∈ On → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)))
77	24, 76	ax-mp 5	. . . . . . 7 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅))
78		opex 5431	. . . . . . . . 9 ⊢ ⟨𝑁, 𝑦⟩ ∈ V
79	78	rdg0 8392	. . . . . . . 8 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅) = ⟨𝑁, 𝑦⟩
80	79	fveq2i 6870	. . . . . . 7 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)) = (𝐹‘⟨𝑁, 𝑦⟩)
81	75, 77, 80	3eqtri 2789	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (𝐹‘⟨𝑁, 𝑦⟩)
82		finxpreclem4.1	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
83	82	finxpreclem3 37887	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ⟨∪ 𝑁, (1st ‘𝑦)⟩ = (𝐹‘⟨𝑁, 𝑦⟩))
84	81, 83	eqtr4id 2816	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = ⟨∪ 𝑁, (1st ‘𝑦)⟩)
85	84	fveq2d 6871	. . . 4 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩))
86		2on0 8452	. . . . . 6 ⊢ 2o ≠ ∅
87		nnlim 7860	. . . . . . 7 ⊢ (2o ∈ ω → ¬ Lim 2o)
88	1, 87	ax-mp 5	. . . . . 6 ⊢ ¬ Lim 2o
89		rdgsucuni 37863	. . . . . 6 ⊢ ((2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)))
90	3, 86, 88, 89	mp3an 1482	. . . . 5 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
91		1oequni2o 37862	. . . . . . 7 ⊢ 1o = ∪ 2o
92	91	fveq2i 6870	. . . . . 6 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o)
93	92	fveq2i 6870	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∪ 2o))
94	90, 93	eqtr4i 2788	. . . 4 ⊢ (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o))
95	74	fveq2i 6870	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅)
96		rdgsuc 8395	. . . . . 6 ⊢ (∅ ∈ On → (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)))
97	24, 96	ax-mp 5	. . . . 5 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅))
98		opex 5431	. . . . . . 7 ⊢ ⟨∪ 𝑁, (1st ‘𝑦)⟩ ∈ V
99	98	rdg0 8392	. . . . . 6 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅) = ⟨∪ 𝑁, (1st ‘𝑦)⟩
100	99	fveq2i 6870	. . . . 5 ⊢ (𝐹‘(rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∅)) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
101	95, 97, 100	3eqtri 2789	. . . 4 ⊢ (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o) = (𝐹‘⟨∪ 𝑁, (1st ‘𝑦)⟩)
102	85, 94, 101	3eqtr4g 2822	. . 3 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘1o))
103		1on 8450	. . . 4 ⊢ 1o ∈ On
104		rdgeqoa 37864	. . . 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 1472	. . 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 6871	. . 3 ⊢ ((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
108	107	adantr 484	. 2 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (℩𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
109	72, 106, 108	3eqtr2rd 2804	1 ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  ∃!wreu 3365  Vcvv 3454  [wsbc 3744  ⦋csb 3852   ⊆ wss 3904  ∅c0 4285  ifcif 4480  ⟨cop 4588  ∪ cuni 4865   × cxp 5645  Ord word 6345  Oncon0 6346  Lim wlim 6347  suc csuc 6348  ‘cfv 6521  ℩crio 7352  (class class class)co 7396   ∈ cmpo 7398  ωcom 7846  1^st c1st 7968  reccrdg 8380  1_oc1o 8430  2_oc2o 8431   +_o coa 8434  Fincfn 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-2o 8438  df-oadd 8441  df-en 8928  df-fin 8931

This theorem is referenced by:  finxpsuclem  37891