Metamath Proof Explorer


Theorem sn1dom

Description: A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023)

Ref Expression
Assertion sn1dom { 𝐴 } ≼ 1o

Proof

Step Hyp Ref Expression
1 ensn1g ( 𝐴 ∈ V → { 𝐴 } ≈ 1o )
2 1on 1o ∈ On
3 domrefg ( 1o ∈ On → 1o ≼ 1o )
4 2 3 ax-mp 1o ≼ 1o
5 endomtr ( ( { 𝐴 } ≈ 1o ∧ 1o ≼ 1o ) → { 𝐴 } ≼ 1o )
6 1 4 5 sylancl ( 𝐴 ∈ V → { 𝐴 } ≼ 1o )
7 snprc ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
8 snex { 𝐴 } ∈ V
9 eqeng ( { 𝐴 } ∈ V → ( { 𝐴 } = ∅ → { 𝐴 } ≈ ∅ ) )
10 8 9 ax-mp ( { 𝐴 } = ∅ → { 𝐴 } ≈ ∅ )
11 7 10 sylbi ( ¬ 𝐴 ∈ V → { 𝐴 } ≈ ∅ )
12 0domg ( 1o ∈ On → ∅ ≼ 1o )
13 2 12 ax-mp ∅ ≼ 1o
14 endomtr ( ( { 𝐴 } ≈ ∅ ∧ ∅ ≼ 1o ) → { 𝐴 } ≼ 1o )
15 11 13 14 sylancl ( ¬ 𝐴 ∈ V → { 𝐴 } ≼ 1o )
16 6 15 pm2.61i { 𝐴 } ≼ 1o