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

Metamath Proof Explorer

Theorem 0sdom1dom

Description: Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un , see 0sdom1domALT . (Contributed by NM, 28-Sep-2004) Avoid ax-un . (Revised by BTernaryTau, 7-Dec-2024)

Ref Expression
Assertion 0sdom1dom 
|- ( (/) ~< A <-> 1o ~<_ A )

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  Rel ~<
2 1 brrelex2i 
 |-  ( (/) ~< A -> A e. _V )
3 reldom 
 |-  Rel ~<_
4 3 brrelex2i 
 |-  ( 1o ~<_ A -> A e. _V )
5 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
6 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
7 snssi 
 |-  ( x e. A -> { x } C_ A )
8 df1o2 
 |-  1o = { (/) }
9 0ex 
 |-  (/) e. _V
10 vex 
 |-  x e. _V
11 en2sn 
 |-  ( ( (/) e. _V /\ x e. _V ) -> { (/) } ~~ { x } )
12 9 10 11 mp2an 
 |-  { (/) } ~~ { x }
13 8 12 eqbrtri 
 |-  1o ~~ { x }
14 endom 
 |-  ( 1o ~~ { x } -> 1o ~<_ { x } )
15 13 14 ax-mp 
 |-  1o ~<_ { x }
16 domssr 
 |-  ( ( A e. _V /\ { x } C_ A /\ 1o ~<_ { x } ) -> 1o ~<_ A )
17 15 16 mp3an3 
 |-  ( ( A e. _V /\ { x } C_ A ) -> 1o ~<_ A )
18 17 ex 
 |-  ( A e. _V -> ( { x } C_ A -> 1o ~<_ A ) )
19 7 18 syl5 
 |-  ( A e. _V -> ( x e. A -> 1o ~<_ A ) )
20 19 exlimdv 
 |-  ( A e. _V -> ( E. x x e. A -> 1o ~<_ A ) )
21 6 20 biimtrid 
 |-  ( A e. _V -> ( A =/= (/) -> 1o ~<_ A ) )
22 1n0 
 |-  1o =/= (/)
23 dom0 
 |-  ( 1o ~<_ (/) <-> 1o = (/) )
24 22 23 nemtbir 
 |-  -. 1o ~<_ (/)
25 breq2 
 |-  ( A = (/) -> ( 1o ~<_ A <-> 1o ~<_ (/) ) )
26 24 25 mtbiri 
 |-  ( A = (/) -> -. 1o ~<_ A )
27 26 necon2ai 
 |-  ( 1o ~<_ A -> A =/= (/) )
28 21 27 impbid1 
 |-  ( A e. _V -> ( A =/= (/) <-> 1o ~<_ A ) )
29 5 28 bitrd 
 |-  ( A e. _V -> ( (/) ~< A <-> 1o ~<_ A ) )
30 2 4 29 pm5.21nii 
 |-  ( (/) ~< A <-> 1o ~<_ A )