This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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