finxpreclem6 - Mathbox for ML

	Mathbox for ML		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > finxpreclem6		Structured version Visualization version GIF version

Theorem finxpreclem6 33233

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

**Hypothesis**
Ref	Expression
finxpreclem5.1	⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))

**Assertion**
Ref	Expression
finxpreclem6	⊢ ((𝑁 ∈ ω ∧ 1_𝑜 ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))

Distinct variable groups: 𝑥,𝑛,𝑁 𝑈,𝑛,𝑥 Allowed substitution hints: 𝐹(𝑥,𝑛)

Proof of Theorem finxpreclem6 Dummy variables 𝑚 𝑜 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2689	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝑛 ∈ ω ↔ 𝑁 ∈ ω))
2		eleq2 2690	. . . . 5 ⊢ (𝑛 = 𝑁 → (1_𝑜 ∈ 𝑛 ↔ 1_𝑜 ∈ 𝑁))
3	1, 2	anbi12d 747	. . . 4 ⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ↔ (𝑁 ∈ ω ∧ 1_𝑜 ∈ 𝑁)))
4		anass 681	. . . . . . . . 9 ⊢ (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑦 ∈ (V × 𝑈)) ↔ (𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))))
5		nfv 1843	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))
6		finxpreclem5.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
7		nfmpt22 6723	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
8	6, 7	nfcxfr 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐹
9		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥⟨𝑛, 𝑦⟩
10	8, 9	nfrdg 7510	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥rec(𝐹, ⟨𝑛, 𝑦⟩)
11		nfcv 2764	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥𝑛
12	10, 11	nffv 6198	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)
13	12	nfeq2 2780	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)
14	13	nfn 1784	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)
15	5, 14	nfim 1825	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))
16		eleq1 2689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (V × 𝑈) ↔ 𝑦 ∈ (V × 𝑈)))
17	16	notbid 308	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ (V × 𝑈) ↔ ¬ 𝑦 ∈ (V × 𝑈)))
18	17	anbi2d 740	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈)) ↔ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))))
19	18	anbi2d 740	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) ↔ (𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))))
20		opeq2 4403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ⟨𝑛, 𝑥⟩ = ⟨𝑛, 𝑦⟩)
21		rdgeq2 7508	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑛, 𝑥⟩ = ⟨𝑛, 𝑦⟩ → rec(𝐹, ⟨𝑛, 𝑥⟩) = rec(𝐹, ⟨𝑛, 𝑦⟩))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → rec(𝐹, ⟨𝑛, 𝑥⟩) = rec(𝐹, ⟨𝑛, 𝑦⟩))
23	22	fveq1d 6193	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))
24	23	eqeq2d 2632	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (∅ = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) ↔ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)))
25	24	notbid 308	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) ↔ ¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)))
26	19, 25	imbi12d 334	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛)) ↔ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))))
27		anass 681	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) ↔ (𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))))
28		vex 3203	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑛 ∈ V
29		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = ∅ → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘∅))
30	29	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = ∅ → ((rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = ⟨𝑛, 𝑥⟩ ↔ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘∅) = ⟨𝑛, 𝑥⟩))
31		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑜 → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜))
32	31	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑜 → ((rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = ⟨𝑛, 𝑥⟩ ↔ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜) = ⟨𝑛, 𝑥⟩))
33		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = suc 𝑜 → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜))
34	33	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = suc 𝑜 → ((rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = ⟨𝑛, 𝑥⟩ ↔ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜) = ⟨𝑛, 𝑥⟩))
35		opex 4932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ⟨𝑛, 𝑥⟩ ∈ V
36	35	rdg0 7517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘∅) = ⟨𝑛, 𝑥⟩
37	36	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘∅) = ⟨𝑛, 𝑥⟩)
38		nnon 7071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑜 ∈ ω → 𝑜 ∈ On)
39		rdgsuc 7520	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑜 ∈ On → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜) = (𝐹‘(rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜)))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑜 ∈ ω → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜) = (𝐹‘(rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜)))
41		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜) = ⟨𝑛, 𝑥⟩ → (𝐹‘(rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜)) = (𝐹‘⟨𝑛, 𝑥⟩))
42	40, 41	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑜 ∈ ω ∧ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜) = ⟨𝑛, 𝑥⟩) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜) = (𝐹‘⟨𝑛, 𝑥⟩))
43	6	finxpreclem5 33232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) → (¬ 𝑥 ∈ (V × 𝑈) → (𝐹‘⟨𝑛, 𝑥⟩) = ⟨𝑛, 𝑥⟩))
44	43	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (𝐹‘⟨𝑛, 𝑥⟩) = ⟨𝑛, 𝑥⟩)
45	42, 44	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑜 ∈ ω ∧ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜) = ⟨𝑛, 𝑥⟩) ∧ ((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜) = ⟨𝑛, 𝑥⟩)
46	45	expl 648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑜 ∈ ω → (((rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜) = ⟨𝑛, 𝑥⟩ ∧ ((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜) = ⟨𝑛, 𝑥⟩))
47	46	expcomd 454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑜 ∈ ω → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → ((rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑜) = ⟨𝑛, 𝑥⟩ → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘suc 𝑜) = ⟨𝑛, 𝑥⟩)))
48	30, 32, 34, 37, 47	finds2 7094	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = ⟨𝑛, 𝑥⟩))
49		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ ω ↔ 𝑚 ∈ ω))
50		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚))
51	50	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → ((rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩ ↔ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = ⟨𝑛, 𝑥⟩))
52	51	imbi2d 330	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩) ↔ (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = ⟨𝑛, 𝑥⟩)))
53	49, 52	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → ((𝑛 ∈ ω → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩)) ↔ (𝑚 ∈ ω → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑚) = ⟨𝑛, 𝑥⟩))))
54	48, 53	mpbiri 248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ ω → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩)))
55	54	equcoms 1947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝑛 ∈ ω → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩)))
56	28, 55	vtocle 3282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩))
57	27, 56	syl5bir 233	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩))
58	57	anabsi5 858	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) = ⟨𝑛, 𝑥⟩)
59		vex 3203	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ∈ V
60	28, 59	opnzi 4943	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨𝑛, 𝑥⟩ ≠ ∅
61	60	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → ⟨𝑛, 𝑥⟩ ≠ ∅)
62	58, 61	eqnetrd 2861	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛) ≠ ∅)
63	62	necomd 2849	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → ∅ ≠ (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛))
64	63	neneqd 2799	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑥⟩)‘𝑛))
65	15, 26, 64	chvar 2262	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))
66	65	intnand 962	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)))
67	66	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) → ¬ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)))
68		abid 2610	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))} ↔ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)))
69		opeq1 4402	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑁 → ⟨𝑛, 𝑦⟩ = ⟨𝑁, 𝑦⟩)
70		rdgeq2 7508	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑛, 𝑦⟩ = ⟨𝑁, 𝑦⟩ → rec(𝐹, ⟨𝑛, 𝑦⟩) = rec(𝐹, ⟨𝑁, 𝑦⟩))
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑁 → rec(𝐹, ⟨𝑛, 𝑦⟩) = rec(𝐹, ⟨𝑁, 𝑦⟩))
72		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁)
73	71, 72	fveq12d 6197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑁 → (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
74	73	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑁 → (∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛) ↔ ∅ = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁)))
75	1, 74	anbi12d 747	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛)) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))))
76	75	abbidv 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑁 → {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))} = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))})
77	6	dffinxpf 33222	. . . . . . . . . . . . . . 15 ⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))}
78	76, 77	syl6eqr 2674	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑁 → {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))} = (𝑈↑↑𝑁))
79	78	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (𝑦 ∈ {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))} ↔ 𝑦 ∈ (𝑈↑↑𝑁)))
80	68, 79	syl5rbbr 275	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (𝑦 ∈ (𝑈↑↑𝑁) ↔ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))))
81	80	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) → (𝑦 ∈ (𝑈↑↑𝑁) ↔ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑛, 𝑦⟩)‘𝑛))))
82	67, 81	mtbird 315	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) → ¬ 𝑦 ∈ (𝑈↑↑𝑁))
83	82	ex 450	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ (1_𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ 𝑦 ∈ (𝑈↑↑𝑁)))
84	4, 83	syl5bi 232	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) ∧ ¬ 𝑦 ∈ (V × 𝑈)) → ¬ 𝑦 ∈ (𝑈↑↑𝑁)))
85	84	expdimp 453	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛)) → (¬ 𝑦 ∈ (V × 𝑈) → ¬ 𝑦 ∈ (𝑈↑↑𝑁)))
86	85	con4d 114	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛)) → (𝑦 ∈ (𝑈↑↑𝑁) → 𝑦 ∈ (V × 𝑈)))
87	86	ssrdv 3609	. . . . 5 ⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛)) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))
88	87	ex 450	. . . 4 ⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ 1_𝑜 ∈ 𝑛) → (𝑈↑↑𝑁) ⊆ (V × 𝑈)))
89	3, 88	sylbird 250	. . 3 ⊢ (𝑛 = 𝑁 → ((𝑁 ∈ ω ∧ 1_𝑜 ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈)))
90	89	vtocleg 3279	. 2 ⊢ (𝑁 ∈ ω → ((𝑁 ∈ ω ∧ 1_𝑜 ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈)))
91	90	anabsi5 858	1 ⊢ ((𝑁 ∈ ω ∧ 1_𝑜 ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 {cab 2608 ≠ wne 2794 Vcvv 3200 ⊆ wss 3574 ∅c0 3915 ifcif 4086 ⟨cop 4183 ∪ cuni 4436 × cxp 5112 Oncon0 5723 suc csuc 5725 ‘cfv 5888 ↦ cmpt2 6652 ωcom 7065 1^st c1st 7166 reccrdg 7505 1_𝑜c1o 7553 ↑↑cfinxp 33220

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-finxp 33221

This theorem is referenced by: finxpsuclem 33234

W3C validator