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

Metamath Proof Explorer

Theorem rex2dom

Description: A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024)

Ref Expression
Assertion rex2dom 
|- ( ( A e. V /\ E. x e. A E. y e. A x =/= y ) -> 2o ~<_ A )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 prssi 
 |-  ( ( x e. A /\ y e. A ) -> { x , y } C_ A )
3 df2o3 
 |-  2o = { (/) , 1o }
4 0ex 
 |-  (/) e. _V
5 4 a1i 
 |-  ( x =/= y -> (/) e. _V )
6 1oex 
 |-  1o e. _V
7 6 a1i 
 |-  ( x =/= y -> 1o e. _V )
8 vex 
 |-  x e. _V
9 8 a1i 
 |-  ( x =/= y -> x e. _V )
10 vex 
 |-  y e. _V
11 10 a1i 
 |-  ( x =/= y -> y e. _V )
12 1n0 
 |-  1o =/= (/)
13 12 necomi 
 |-  (/) =/= 1o
14 13 a1i 
 |-  ( x =/= y -> (/) =/= 1o )
15 id 
 |-  ( x =/= y -> x =/= y )
16 5 7 9 11 14 15 en2prd 
 |-  ( x =/= y -> { (/) , 1o } ~~ { x , y } )
17 3 16 eqbrtrid 
 |-  ( x =/= y -> 2o ~~ { x , y } )
18 endom 
 |-  ( 2o ~~ { x , y } -> 2o ~<_ { x , y } )
19 17 18 syl 
 |-  ( x =/= y -> 2o ~<_ { x , y } )
20 domssr 
 |-  ( ( A e. _V /\ { x , y } C_ A /\ 2o ~<_ { x , y } ) -> 2o ~<_ A )
21 20 3expib 
 |-  ( A e. _V -> ( ( { x , y } C_ A /\ 2o ~<_ { x , y } ) -> 2o ~<_ A ) )
22 2 19 21 syl2ani 
 |-  ( A e. _V -> ( ( ( x e. A /\ y e. A ) /\ x =/= y ) -> 2o ~<_ A ) )
23 22 expd 
 |-  ( A e. _V -> ( ( x e. A /\ y e. A ) -> ( x =/= y -> 2o ~<_ A ) ) )
24 23 rexlimdvv 
 |-  ( A e. _V -> ( E. x e. A E. y e. A x =/= y -> 2o ~<_ A ) )
25 1 24 syl 
 |-  ( A e. V -> ( E. x e. A E. y e. A x =/= y -> 2o ~<_ A ) )
26 25 imp 
 |-  ( ( A e. V /\ E. x e. A E. y e. A x =/= y ) -> 2o ~<_ A )