Metamath Proof Explorer


Theorem 0sdom1dom

Description: Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un , see 0sdom1domALT . (Contributed by NM, 28-Sep-2004) Avoid ax-un . (Revised by BTernaryTau, 7-Dec-2024)

Ref Expression
Assertion 0sdom1dom A 1 𝑜 A

Proof

Step Hyp Ref Expression
1 relsdom Rel
2 1 brrelex2i A A V
3 reldom Rel
4 3 brrelex2i 1 𝑜 A A V
5 0sdomg A V A A
6 n0 A x x A
7 snssi x A x A
8 df1o2 1 𝑜 =
9 0ex V
10 vex x V
11 en2sn V x V x
12 9 10 11 mp2an x
13 8 12 eqbrtri 1 𝑜 x
14 endom 1 𝑜 x 1 𝑜 x
15 13 14 ax-mp 1 𝑜 x
16 domssr A V x A 1 𝑜 x 1 𝑜 A
17 15 16 mp3an3 A V x A 1 𝑜 A
18 17 ex A V x A 1 𝑜 A
19 7 18 syl5 A V x A 1 𝑜 A
20 19 exlimdv A V x x A 1 𝑜 A
21 6 20 biimtrid A V A 1 𝑜 A
22 1n0 1 𝑜
23 dom0 1 𝑜 1 𝑜 =
24 22 23 nemtbir ¬ 1 𝑜
25 breq2 A = 1 𝑜 A 1 𝑜
26 24 25 mtbiri A = ¬ 1 𝑜 A
27 26 necon2ai 1 𝑜 A A
28 21 27 impbid1 A V A 1 𝑜 A
29 5 28 bitrd A V A 1 𝑜 A
30 2 4 29 pm5.21nii A 1 𝑜 A