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