Theorem axprOLD

Description: Obsolete version of axpr as of 18-Sep-2025. (Contributed by NM, 14-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axprOLD	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		axprlem3OLD	⊢ ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
2		biimpr	⊢ ( ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) )
3	2	alimi	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) )
4	1 3	eximii	⊢ ∃ 𝑧 ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 )
5		axprlem4OLD	⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
6		axprlem5OLD	⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
7	5 6	jaodan	⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
8	7	ex	⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
9	8	imim1d	⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) )
10	9	alimdv	⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) )
11	10	eximdv	⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ∃ 𝑧 ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) )
12	4 11	mpi	⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) )
13		axprlem2	⊢ ∃ 𝑝 ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 )
14	12 13	exlimiiv	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )