finxpsuclem - Mathbox for ML

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

Theorem finxpsuclem 38102

Description: Lemma for finxpsuc 38103. (Contributed by ML, 24-Oct-2020.)

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

**Assertion**
Ref	Expression
finxpsuclem	⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))

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

Proof of Theorem finxpsuclem Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano2 7892	. . . . . . . . . 10 ⊢ (𝑁 ∈ ω → suc 𝑁 ∈ ω)
2	1	adantr 486	. . . . . . . . 9 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → suc 𝑁 ∈ ω)
3		1on 8472	. . . . . . . . . . . . 13 ⊢ 1_o ∈ On
4	3	onordi 6478	. . . . . . . . . . . 12 ⊢ Ord 1_o
5		nnord 7876	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → Ord 𝑁)
6		ordsseleq 6394	. . . . . . . . . . . 12 ⊢ ((Ord 1_o ∧ Ord 𝑁) → (1_o ⊆ 𝑁 ↔ (1_o ∈ 𝑁 ∨ 1_o = 𝑁)))
7	4, 5, 6	sylancr 599	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → (1_o ⊆ 𝑁 ↔ (1_o ∈ 𝑁 ∨ 1_o = 𝑁)))
8	7	biimpa 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (1_o ∈ 𝑁 ∨ 1_o = 𝑁))
9		elelsuc 6440	. . . . . . . . . . . . 13 ⊢ (1_o ∈ 𝑁 → 1_o ∈ suc 𝑁)
10	9	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → (1_o ∈ 𝑁 → 1_o ∈ suc 𝑁))
11		sucidg 6448	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → 𝑁 ∈ suc 𝑁)
12		eleq1 2853	. . . . . . . . . . . . 13 ⊢ (1_o = 𝑁 → (1_o ∈ suc 𝑁 ↔ 𝑁 ∈ suc 𝑁))
13	11, 12	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → (1_o = 𝑁 → 1_o ∈ suc 𝑁))
14	10, 13	jaod 873	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → ((1_o ∈ 𝑁 ∨ 1_o = 𝑁) → 1_o ∈ suc 𝑁))
15	14	adantr 486	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → ((1_o ∈ 𝑁 ∨ 1_o = 𝑁) → 1_o ∈ suc 𝑁))
16	8, 15	mpd 16	. . . . . . . . 9 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → 1_o ∈ suc 𝑁)
17		finxpsuclem.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
18	17	finxpreclem6 38101	. . . . . . . . 9 ⊢ ((suc 𝑁 ∈ ω ∧ 1_o ∈ suc 𝑁) → (𝑈↑↑suc 𝑁) ⊆ (V × 𝑈))
19	2, 16, 18	syl2anc 596	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑈↑↑suc 𝑁) ⊆ (V × 𝑈))
20	19	sselda 3938	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → 𝑦 ∈ (V × 𝑈))
21	1	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → suc 𝑁 ∈ ω)
22		df-2o 8460	. . . . . . . . . . . . . . 15 ⊢ 2_o = suc 1_o
23		ordsucsssuc 7825	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 1_o ∧ Ord 𝑁) → (1_o ⊆ 𝑁 ↔ suc 1_o ⊆ suc 𝑁))
24	4, 5, 23	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ω → (1_o ⊆ 𝑁 ↔ suc 1_o ⊆ suc 𝑁))
25	24	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → suc 1_o ⊆ suc 𝑁)
26	22, 25	eqsstrid 3976	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → 2_o ⊆ suc 𝑁)
27	26	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 2_o ⊆ suc 𝑁)
28		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 𝑦 ∈ (V × 𝑈))
29	17	finxpreclem4 38099	. . . . . . . . . . . . 13 ⊢ (((suc 𝑁 ∈ ω ∧ 2_o ⊆ suc 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) = (rec(𝐹, ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩)‘∪ suc 𝑁))
30	21, 27, 28, 29	syl21anc 851	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) = (rec(𝐹, ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩)‘∪ suc 𝑁))
31		ordunisuc 7834	. . . . . . . . . . . . . . . 16 ⊢ (Ord 𝑁 → ∪ suc 𝑁 = 𝑁)
32	5, 31	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ω → ∪ suc 𝑁 = 𝑁)
33		opeq1 4840	. . . . . . . . . . . . . . . 16 ⊢ (∪ suc 𝑁 = 𝑁 → ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩ = ⟨𝑁, (1^st ‘𝑦)⟩)
34		rdgeq2 8405	. . . . . . . . . . . . . . . 16 ⊢ (⟨∪ suc 𝑁, (1^st ‘𝑦)⟩ = ⟨𝑁, (1^st ‘𝑦)⟩ → rec(𝐹, ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩) = rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩))
35	33, 34	syl 18	. . . . . . . . . . . . . . 15 ⊢ (∪ suc 𝑁 = 𝑁 → rec(𝐹, ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩) = rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩))
36	32, 35	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ω → rec(𝐹, ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩) = rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩))
37	36, 32	fveq12d 6892	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → (rec(𝐹, ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩)‘∪ suc 𝑁) = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁))
38	37	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨∪ suc 𝑁, (1^st ‘𝑦)⟩)‘∪ suc 𝑁) = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁))
39	30, 38	eqtrd 2800	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁))
40	39	eqeq2d 2776	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁)))
41	17	dffinxpf 38090	. . . . . . . . . . . . 13 ⊢ (𝑈↑↑suc 𝑁) = {𝑦 ∣ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁))}
42	41	eqabri 2907	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁)))
43	1	biantrurd 542	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → (∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁) ↔ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁))))
44	42, 43	bitr4id 293	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁)))
45	44	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ∅ = (rec(𝐹, ⟨suc 𝑁, 𝑦⟩)‘suc 𝑁)))
46		fvex 6898	. . . . . . . . . . . . 13 ⊢ (1^st ‘𝑦) ∈ V
47		opeq2 4841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (1^st ‘𝑦) → ⟨𝑁, 𝑧⟩ = ⟨𝑁, (1^st ‘𝑦)⟩)
48		rdgeq2 8405	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑁, 𝑧⟩ = ⟨𝑁, (1^st ‘𝑦)⟩ → rec(𝐹, ⟨𝑁, 𝑧⟩) = rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩))
49	47, 48	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1^st ‘𝑦) → rec(𝐹, ⟨𝑁, 𝑧⟩) = rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩))
50	49	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1^st ‘𝑦) → (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁) = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁))
51	50	eqeq2d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (1^st ‘𝑦) → (∅ = (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁)))
52	51	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑧 = (1^st ‘𝑦) → ((𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁)) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁))))
53	17	dffinxpf 38090	. . . . . . . . . . . . 13 ⊢ (𝑈↑↑𝑁) = {𝑧 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑧⟩)‘𝑁))}
54	46, 52, 53	elab2 3643	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁)))
55	54	baib 545	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → ((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁)))
56	55	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) ↔ ∅ = (rec(𝐹, ⟨𝑁, (1^st ‘𝑦)⟩)‘𝑁)))
57	40, 45, 56	3bitr4d 314	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ (1^st ‘𝑦) ∈ (𝑈↑↑𝑁)))
58	57	biimpd 232	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → (1^st ‘𝑦) ∈ (𝑈↑↑𝑁)))
59	58	impancom 457	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → (𝑦 ∈ (V × 𝑈) → (1^st ‘𝑦) ∈ (𝑈↑↑𝑁)))
60	20, 59	mpd 16	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) ∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → (1^st ‘𝑦) ∈ (𝑈↑↑𝑁))
61	60	ex 418	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → (1^st ‘𝑦) ∈ (𝑈↑↑𝑁)))
62	20	ex 418	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → 𝑦 ∈ (V × 𝑈)))
63	61, 62	jcad 522	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → ((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈))))
64	57	exbiri 823	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑦 ∈ (V × 𝑈) → ((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) → 𝑦 ∈ (𝑈↑↑suc 𝑁))))
65	64	impd 416	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → ((𝑦 ∈ (V × 𝑈) ∧ (1^st ‘𝑦) ∈ (𝑈↑↑𝑁)) → 𝑦 ∈ (𝑈↑↑suc 𝑁)))
66	65	ancomsd 471	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 𝑦 ∈ (𝑈↑↑suc 𝑁)))
67	63, 66	impbid 215	. . 3 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈))))
68		elxp8 38076	. . 3 ⊢ (𝑦 ∈ ((𝑈↑↑𝑁) × 𝑈) ↔ ((1^st ‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈)))
69	67, 68	bitr4di 292	. 2 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ 𝑦 ∈ ((𝑈↑↑𝑁) × 𝑈)))
70	69	eqrdv 2763	1 ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2146 Vcvv 3457 ⊆ wss 3906 ∅c0 4286 ifcif 4489 ⟨cop 4597 ∪ cuni 4874 × cxp 5661 Ord word 6363 suc csuc 6366 ‘cfv 6540 ∈ cmpo 7421 ωcom 7868 1^st c1st 7990 reccrdg 8402 1_oc1o 8452 2_oc2o 8453 ↑↑cfinxp 38088

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pr 5406 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-en 8950 df-fin 8953 df-finxp 38089

This theorem is used by: finxpsuc 38103

W3C validator