Theorem snnen2o

Description: A singleton { A } is never equinumerous with the ordinal number 2. This holds for proper singletons ( A e.V ) as well as for singletons being the empty set ( A e/ V ). (Contributed by AV, 6-Aug-2019)

	Ref	Expression
Assertion	snnen2o	⊢ ¬ { 𝐴 } ≈ 2o

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2		php5	⊢ ( 1o ∈ ω → ¬ 1o ≈ suc 1o )
3	1 2	ax-mp	⊢ ¬ 1o ≈ suc 1o
4		ensn1g	⊢ ( 𝐴 ∈ V → { 𝐴 } ≈ 1o )
5		df-2o	⊢ 2o = suc 1o
6	5	eqcomi	⊢ suc 1o = 2o
7	6	breq2i	⊢ ( 1o ≈ suc 1o ↔ 1o ≈ 2o )
8		ensymb	⊢ ( { 𝐴 } ≈ 1o ↔ 1o ≈ { 𝐴 } )
9		entr	⊢ ( ( 1o ≈ { 𝐴 } ∧ { 𝐴 } ≈ 2o ) → 1o ≈ 2o )
10	9	ex	⊢ ( 1o ≈ { 𝐴 } → ( { 𝐴 } ≈ 2o → 1o ≈ 2o ) )
11	8 10	sylbi	⊢ ( { 𝐴 } ≈ 1o → ( { 𝐴 } ≈ 2o → 1o ≈ 2o ) )
12	11	con3rr3	⊢ ( ¬ 1o ≈ 2o → ( { 𝐴 } ≈ 1o → ¬ { 𝐴 } ≈ 2o ) )
13	7 12	sylnbi	⊢ ( ¬ 1o ≈ suc 1o → ( { 𝐴 } ≈ 1o → ¬ { 𝐴 } ≈ 2o ) )
14	3 4 13	mpsyl	⊢ ( 𝐴 ∈ V → ¬ { 𝐴 } ≈ 2o )
15		2on0	⊢ 2o ≠ ∅
16		ensymb	⊢ ( ∅ ≈ 2o ↔ 2o ≈ ∅ )
17		en0	⊢ ( 2o ≈ ∅ ↔ 2o = ∅ )
18	16 17	bitri	⊢ ( ∅ ≈ 2o ↔ 2o = ∅ )
19	15 18	nemtbir	⊢ ¬ ∅ ≈ 2o
20		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
21	20	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
22	21	breq1d	⊢ ( ¬ 𝐴 ∈ V → ( { 𝐴 } ≈ 2o ↔ ∅ ≈ 2o ) )
23	19 22	mtbiri	⊢ ( ¬ 𝐴 ∈ V → ¬ { 𝐴 } ≈ 2o )
24	14 23	pm2.61i	⊢ ¬ { 𝐴 } ≈ 2o