Metamath Proof Explorer


Theorem sn1dom

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

Ref Expression
Assertion sn1dom A 1 𝑜

Proof

Step Hyp Ref Expression
1 ensn1g A V A 1 𝑜
2 1on 1 𝑜 On
3 domrefg 1 𝑜 On 1 𝑜 1 𝑜
4 2 3 ax-mp 1 𝑜 1 𝑜
5 endomtr A 1 𝑜 1 𝑜 1 𝑜 A 1 𝑜
6 1 4 5 sylancl A V A 1 𝑜
7 snprc ¬ A V A =
8 snex A V
9 eqeng A V A = A
10 8 9 ax-mp A = A
11 7 10 sylbi ¬ A V A
12 0domg 1 𝑜 On 1 𝑜
13 2 12 ax-mp 1 𝑜
14 endomtr A 1 𝑜 A 1 𝑜
15 11 13 14 sylancl ¬ A V A 1 𝑜
16 6 15 pm2.61i A 1 𝑜