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

Metamath Proof Explorer

Theorem 1sdom2dom

Description: Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024)

Ref Expression
Assertion 1sdom2dom 
|- ( 1o ~< A <-> 2o ~<_ A )

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  Rel ~<
2 1 brrelex2i 
 |-  ( 1o ~< A -> A e. _V )
3 sdomdom 
 |-  ( 1o ~< A -> 1o ~<_ A )
4 0sdom1dom 
 |-  ( (/) ~< A <-> 1o ~<_ A )
5 3 4 sylibr 
 |-  ( 1o ~< A -> (/) ~< A )
6 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
7 2 6 syl 
 |-  ( 1o ~< A -> ( (/) ~< A <-> A =/= (/) ) )
8 5 7 mpbid 
 |-  ( 1o ~< A -> A =/= (/) )
9 n0snor2el 
 |-  ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. x A = { x } ) )
10 8 9 syl 
 |-  ( 1o ~< A -> ( E. x e. A E. y e. A x =/= y \/ E. x A = { x } ) )
11 sdomnen 
 |-  ( 1o ~< A -> -. 1o ~~ A )
12 df1o2 
 |-  1o = { (/) }
13 0ex 
 |-  (/) e. _V
14 vex 
 |-  x e. _V
15 en2sn 
 |-  ( ( (/) e. _V /\ x e. _V ) -> { (/) } ~~ { x } )
16 13 14 15 mp2an 
 |-  { (/) } ~~ { x }
17 12 16 eqbrtri 
 |-  1o ~~ { x }
18 breq2 
 |-  ( A = { x } -> ( 1o ~~ A <-> 1o ~~ { x } ) )
19 17 18 mpbiri 
 |-  ( A = { x } -> 1o ~~ A )
20 19 exlimiv 
 |-  ( E. x A = { x } -> 1o ~~ A )
21 11 20 nsyl 
 |-  ( 1o ~< A -> -. E. x A = { x } )
22 10 21 olcnd 
 |-  ( 1o ~< A -> E. x e. A E. y e. A x =/= y )
23 rex2dom 
 |-  ( ( A e. _V /\ E. x e. A E. y e. A x =/= y ) -> 2o ~<_ A )
24 2 22 23 syl2anc 
 |-  ( 1o ~< A -> 2o ~<_ A )
25 snsspr1 
 |-  { (/) } C_ { (/) , 1o }
26 df2o3 
 |-  2o = { (/) , 1o }
27 25 12 26 3sstr4i 
 |-  1o C_ 2o
28 domssl 
 |-  ( ( 1o C_ 2o /\ 2o ~<_ A ) -> 1o ~<_ A )
29 27 28 mpan 
 |-  ( 2o ~<_ A -> 1o ~<_ A )
30 snnen2o 
 |-  -. { y } ~~ 2o
31 13 a1i 
 |-  ( T. -> (/) e. _V )
32 1oex 
 |-  1o e. _V
33 32 a1i 
 |-  ( T. -> 1o e. _V )
34 1n0 
 |-  1o =/= (/)
35 34 nesymi 
 |-  -. (/) = 1o
36 35 a1i 
 |-  ( T. -> -. (/) = 1o )
37 31 33 36 enpr2d 
 |-  ( T. -> { (/) , 1o } ~~ 2o )
38 37 mptru 
 |-  { (/) , 1o } ~~ 2o
39 26 38 eqbrtri 
 |-  2o ~~ 2o
40 breq1 
 |-  ( 2o = { y } -> ( 2o ~~ 2o <-> { y } ~~ 2o ) )
41 39 40 mpbii 
 |-  ( 2o = { y } -> { y } ~~ 2o )
42 30 41 mto 
 |-  -. 2o = { y }
43 42 nex 
 |-  -. E. y 2o = { y }
44 2on0 
 |-  2o =/= (/)
45 f1cdmsn 
 |-  ( ( f : 2o -1-1-> { x } /\ 2o =/= (/) ) -> E. y 2o = { y } )
46 44 45 mpan2 
 |-  ( f : 2o -1-1-> { x } -> E. y 2o = { y } )
47 43 46 mto 
 |-  -. f : 2o -1-1-> { x }
48 47 nex 
 |-  -. E. f f : 2o -1-1-> { x }
49 brdomi 
 |-  ( 2o ~<_ { x } -> E. f f : 2o -1-1-> { x } )
50 48 49 mto 
 |-  -. 2o ~<_ { x }
51 breq2 
 |-  ( A = { x } -> ( 2o ~<_ A <-> 2o ~<_ { x } ) )
52 50 51 mtbiri 
 |-  ( A = { x } -> -. 2o ~<_ A )
53 52 con2i 
 |-  ( 2o ~<_ A -> -. A = { x } )
54 53 nexdv 
 |-  ( 2o ~<_ A -> -. E. x A = { x } )
55 reldom 
 |-  Rel ~<_
56 55 brrelex2i 
 |-  ( 2o ~<_ A -> A e. _V )
57 breng 
 |-  ( ( 1o e. _V /\ A e. _V ) -> ( 1o ~~ A <-> E. f f : 1o -1-1-onto-> A ) )
58 32 57 mpan 
 |-  ( A e. _V -> ( 1o ~~ A <-> E. f f : 1o -1-1-onto-> A ) )
59 56 58 syl 
 |-  ( 2o ~<_ A -> ( 1o ~~ A <-> E. f f : 1o -1-1-onto-> A ) )
60 29 4 sylibr 
 |-  ( 2o ~<_ A -> (/) ~< A )
61 56 6 syl 
 |-  ( 2o ~<_ A -> ( (/) ~< A <-> A =/= (/) ) )
62 60 61 mpbid 
 |-  ( 2o ~<_ A -> A =/= (/) )
63 f1ocnv 
 |-  ( f : 1o -1-1-onto-> A -> `' f : A -1-1-onto-> 1o )
64 f1of1 
 |-  ( `' f : A -1-1-onto-> 1o -> `' f : A -1-1-> 1o )
65 f1eq3 
 |-  ( 1o = { (/) } -> ( `' f : A -1-1-> 1o <-> `' f : A -1-1-> { (/) } ) )
66 12 65 ax-mp 
 |-  ( `' f : A -1-1-> 1o <-> `' f : A -1-1-> { (/) } )
67 64 66 sylib 
 |-  ( `' f : A -1-1-onto-> 1o -> `' f : A -1-1-> { (/) } )
68 63 67 syl 
 |-  ( f : 1o -1-1-onto-> A -> `' f : A -1-1-> { (/) } )
69 f1cdmsn 
 |-  ( ( `' f : A -1-1-> { (/) } /\ A =/= (/) ) -> E. x A = { x } )
70 68 69 sylan 
 |-  ( ( f : 1o -1-1-onto-> A /\ A =/= (/) ) -> E. x A = { x } )
71 70 expcom 
 |-  ( A =/= (/) -> ( f : 1o -1-1-onto-> A -> E. x A = { x } ) )
72 71 exlimdv 
 |-  ( A =/= (/) -> ( E. f f : 1o -1-1-onto-> A -> E. x A = { x } ) )
73 62 72 syl 
 |-  ( 2o ~<_ A -> ( E. f f : 1o -1-1-onto-> A -> E. x A = { x } ) )
74 59 73 sylbid 
 |-  ( 2o ~<_ A -> ( 1o ~~ A -> E. x A = { x } ) )
75 54 74 mtod 
 |-  ( 2o ~<_ A -> -. 1o ~~ A )
76 brsdom 
 |-  ( 1o ~< A <-> ( 1o ~<_ A /\ -. 1o ~~ A ) )
77 29 75 76 sylanbrc 
 |-  ( 2o ~<_ A -> 1o ~< A )
78 24 77 impbii 
 |-  ( 1o ~< A <-> 2o ~<_ A )