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

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 ) )