finxpreclem1 - Mathbox for ML

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

Theorem finxpreclem1 33533

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

**Assertion**
Ref	Expression
finxpreclem1	⊢ (𝑋 ∈ 𝑈 → ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))‘⟨1_𝑜, 𝑋⟩))

Distinct variable groups: 𝑈,𝑛,𝑥 𝑛,𝑋,𝑥

**Proof of Theorem finxpreclem1**
Step	Hyp	Ref	Expression
1		df-ov 6812	. 2 ⊢ (1_𝑜(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))𝑋) = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))‘⟨1_𝑜, 𝑋⟩)
2		eqidd 2757	. . 3 ⊢ (𝑋 ∈ 𝑈 → (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))) = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))))
3		eleq1a 2830	. . . . . 6 ⊢ (𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → 𝑥 ∈ 𝑈))
4	3	anim2d 590	. . . . 5 ⊢ (𝑋 ∈ 𝑈 → ((𝑛 = 1_𝑜 ∧ 𝑥 = 𝑋) → (𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈)))
5		iftrue 4232	. . . . 5 ⊢ ((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈) → if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)) = ∅)
6	4, 5	syl6 35	. . . 4 ⊢ (𝑋 ∈ 𝑈 → ((𝑛 = 1_𝑜 ∧ 𝑥 = 𝑋) → if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)) = ∅))
7	6	imp 444	. . 3 ⊢ ((𝑋 ∈ 𝑈 ∧ (𝑛 = 1_𝑜 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)) = ∅)
8		1onn 7884	. . . 4 ⊢ 1_𝑜 ∈ ω
9	8	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑈 → 1_𝑜 ∈ ω)
10		elex 3348	. . 3 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ V)
11		0ex 4938	. . . 4 ⊢ ∅ ∈ V
12	11	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑈 → ∅ ∈ V)
13	2, 7, 9, 10, 12	ovmpt2d 6949	. 2 ⊢ (𝑋 ∈ 𝑈 → (1_𝑜(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))𝑋) = ∅)
14	1, 13	syl5reqr 2805	1 ⊢ (𝑋 ∈ 𝑈 → ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))‘⟨1_𝑜, 𝑋⟩))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1628 ∈ wcel 2135 Vcvv 3336 ∅c0 4054 ifcif 4226 ⟨cop 4323 ∪ cuni 4584 × cxp 5260 ‘cfv 6045 (class class class)co 6809 ↦ cmpt2 6811 ωcom 7226 1^st c1st 7327 1_𝑜c1o 7718

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pr 5051 ax-un 7110

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-ral 3051 df-rex 3052 df-rab 3055 df-v 3338 df-sbc 3573 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-pss 3727 df-nul 4055 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4585 df-br 4801 df-opab 4861 df-tr 4901 df-id 5170 df-eprel 5175 df-po 5183 df-so 5184 df-fr 5221 df-we 5223 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-ord 5883 df-on 5884 df-lim 5885 df-suc 5886 df-iota 6008 df-fun 6047 df-fv 6053 df-ov 6812 df-oprab 6813 df-mpt2 6814 df-om 7227 df-1o 7725

This theorem is referenced by: finxp1o 33536

W3C validator