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 ( ∅ ≺ 𝐴 ↔ 1o𝐴 )

Proof

Step Hyp Ref Expression
1 relsdom Rel ≺
2 1 brrelex2i ( ∅ ≺ 𝐴𝐴 ∈ V )
3 reldom Rel ≼
4 3 brrelex2i ( 1o𝐴𝐴 ∈ V )
5 0sdomg ( 𝐴 ∈ V → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
6 n0 ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥𝐴 )
7 snssi ( 𝑥𝐴 → { 𝑥 } ⊆ 𝐴 )
8 df1o2 1o = { ∅ }
9 0ex ∅ ∈ V
10 vex 𝑥 ∈ V
11 en2sn ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → { ∅ } ≈ { 𝑥 } )
12 9 10 11 mp2an { ∅ } ≈ { 𝑥 }
13 8 12 eqbrtri 1o ≈ { 𝑥 }
14 endom ( 1o ≈ { 𝑥 } → 1o ≼ { 𝑥 } )
15 13 14 ax-mp 1o ≼ { 𝑥 }
16 domssr ( ( 𝐴 ∈ V ∧ { 𝑥 } ⊆ 𝐴 ∧ 1o ≼ { 𝑥 } ) → 1o𝐴 )
17 15 16 mp3an3 ( ( 𝐴 ∈ V ∧ { 𝑥 } ⊆ 𝐴 ) → 1o𝐴 )
18 17 ex ( 𝐴 ∈ V → ( { 𝑥 } ⊆ 𝐴 → 1o𝐴 ) )
19 7 18 syl5 ( 𝐴 ∈ V → ( 𝑥𝐴 → 1o𝐴 ) )
20 19 exlimdv ( 𝐴 ∈ V → ( ∃ 𝑥 𝑥𝐴 → 1o𝐴 ) )
21 6 20 biimtrid ( 𝐴 ∈ V → ( 𝐴 ≠ ∅ → 1o𝐴 ) )
22 1n0 1o ≠ ∅
23 dom0 ( 1o ≼ ∅ ↔ 1o = ∅ )
24 22 23 nemtbir ¬ 1o ≼ ∅
25 breq2 ( 𝐴 = ∅ → ( 1o𝐴 ↔ 1o ≼ ∅ ) )
26 24 25 mtbiri ( 𝐴 = ∅ → ¬ 1o𝐴 )
27 26 necon2ai ( 1o𝐴𝐴 ≠ ∅ )
28 21 27 impbid1 ( 𝐴 ∈ V → ( 𝐴 ≠ ∅ ↔ 1o𝐴 ) )
29 5 28 bitrd ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 1o𝐴 ) )
30 2 4 29 pm5.21nii ( ∅ ≺ 𝐴 ↔ 1o𝐴 )