Theorem axnulALT

Description: Alternate proof of axnul , proved from propositional calculus, ax-gen , ax-4 , sp , and ax-rep . To check this, replace sp with the obsolete axiom ax-c5 in the proof of axnulALT and type the Metamath program "MM> SHOW TRACE__BACK axnulALT / AXIOMS" command. (Contributed by Jeff Hoffman, 3-Feb-2008) (Proof shortened by Mario Carneiro, 17-Nov-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axnulALT	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		ax-rep	⊢ ( ∀ 𝑤 ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
2		sp	⊢ ( ∀ 𝑥 ¬ ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) → ¬ ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) )
3	2	con2i	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) → ¬ ∀ 𝑥 ¬ ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) )
4		df-ex	⊢ ( ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) ↔ ¬ ∀ 𝑥 ¬ ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) )
5	3 4	sylibr	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) )
6		fal	⊢ ¬ ⊥
7		sp	⊢ ( ∀ 𝑥 ⊥ → ⊥ )
8	6 7	mto	⊢ ¬ ∀ 𝑥 ⊥
9	8	pm2.21i	⊢ ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 )
10	5 9	mpg	⊢ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 )
11	1 10	mpg	⊢ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) )
12	8	intnan	⊢ ¬ ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ )
13	12	nex	⊢ ¬ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ )
14	13	nbn	⊢ ( ¬ 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
15	14	albii	⊢ ( ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
16	15	exbii	⊢ ( ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
17	11 16	mpbir	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥