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