This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥