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 V x A y A x y 2 𝑜 A

Proof

Step Hyp Ref Expression
1 elex A V A V
2 prssi x A y A x y A
3 df2o3 2 𝑜 = 1 𝑜
4 0ex V
5 4 a1i x y V
6 1oex 1 𝑜 V
7 6 a1i x y 1 𝑜 V
8 vex x V
9 8 a1i x y x V
10 vex y V
11 10 a1i x y y V
12 1n0 1 𝑜
13 12 necomi 1 𝑜
14 13 a1i x y 1 𝑜
15 id x y x y
16 5 7 9 11 14 15 en2prd x y 1 𝑜 x y
17 3 16 eqbrtrid x y 2 𝑜 x y
18 endom 2 𝑜 x y 2 𝑜 x y
19 17 18 syl x y 2 𝑜 x y
20 domssr A V x y A 2 𝑜 x y 2 𝑜 A
21 20 3expib A V x y A 2 𝑜 x y 2 𝑜 A
22 2 19 21 syl2ani A V x A y A x y 2 𝑜 A
23 22 expd A V x A y A x y 2 𝑜 A
24 23 rexlimdvv A V x A y A x y 2 𝑜 A
25 1 24 syl A V x A y A x y 2 𝑜 A
26 25 imp A V x A y A x y 2 𝑜 A