Metamath Proof Explorer


Theorem 1sdom

Description: A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom .) (Contributed by Mario Carneiro, 12-Jan-2013) Avoid ax-un . (Revised by BTernaryTau, 30-Dec-2024)

Ref Expression
Assertion 1sdom
|- ( A e. V -> ( 1o ~< A <-> E. x e. A E. y e. A -. x = y ) )

Proof

Step Hyp Ref Expression
1 1sdom2dom
 |-  ( 1o ~< A <-> 2o ~<_ A )
2 2dom
 |-  ( 2o ~<_ A -> E. x e. A E. y e. A -. x = y )
3 df-ne
 |-  ( x =/= y <-> -. x = y )
4 3 2rexbii
 |-  ( E. x e. A E. y e. A x =/= y <-> E. x e. A E. y e. A -. x = y )
5 rex2dom
 |-  ( ( A e. V /\ E. x e. A E. y e. A x =/= y ) -> 2o ~<_ A )
6 4 5 sylan2br
 |-  ( ( A e. V /\ E. x e. A E. y e. A -. x = y ) -> 2o ~<_ A )
7 6 ex
 |-  ( A e. V -> ( E. x e. A E. y e. A -. x = y -> 2o ~<_ A ) )
8 2 7 impbid2
 |-  ( A e. V -> ( 2o ~<_ A <-> E. x e. A E. y e. A -. x = y ) )
9 1 8 bitrid
 |-  ( A e. V -> ( 1o ~< A <-> E. x e. A E. y e. A -. x = y ) )