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 )