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 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}$

Proof

Step Hyp Ref Expression
1 ax-rep ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\perp \right)\right)$
2 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)\to ¬\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)$
3 2 con2i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)$
4 df-ex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)$
5 3 4 sylibr ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)$
6 fal ${⊢}¬\perp$
7 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to \perp$
8 6 7 mto ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\perp$
9 8 pm2.21i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}$
10 5 9 mpg ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\perp \to {y}={x}\right)$
11 1 10 mpg ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\perp \right)\right)$
12 8 intnan ${⊢}¬\left({w}\in {z}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\perp \right)$
13 12 nex ${⊢}¬\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\perp \right)$
14 13 nbn ${⊢}¬{y}\in {x}↔\left({y}\in {x}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\perp \right)\right)$
15 14 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\perp \right)\right)$
16 15 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\perp \right)\right)$
17 11 16 mpbir ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}$