Metamath Proof Explorer


Theorem en1eqsn

Description: A set with one element is a singleton. (Contributed by FL, 18-Aug-2008)

Ref Expression
Assertion en1eqsn ( ( 𝐴𝐵𝐵 ≈ 1o ) → 𝐵 = { 𝐴 } )

Proof

Step Hyp Ref Expression
1 1onn 1o ∈ ω
2 ssid 1o ⊆ 1o
3 ssnnfi ( ( 1o ∈ ω ∧ 1o ⊆ 1o ) → 1o ∈ Fin )
4 1 2 3 mp2an 1o ∈ Fin
5 enfii ( ( 1o ∈ Fin ∧ 𝐵 ≈ 1o ) → 𝐵 ∈ Fin )
6 4 5 mpan ( 𝐵 ≈ 1o𝐵 ∈ Fin )
7 6 adantl ( ( 𝐴𝐵𝐵 ≈ 1o ) → 𝐵 ∈ Fin )
8 snssi ( 𝐴𝐵 → { 𝐴 } ⊆ 𝐵 )
9 8 adantr ( ( 𝐴𝐵𝐵 ≈ 1o ) → { 𝐴 } ⊆ 𝐵 )
10 ensn1g ( 𝐴𝐵 → { 𝐴 } ≈ 1o )
11 ensym ( 𝐵 ≈ 1o → 1o𝐵 )
12 entr ( ( { 𝐴 } ≈ 1o ∧ 1o𝐵 ) → { 𝐴 } ≈ 𝐵 )
13 10 11 12 syl2an ( ( 𝐴𝐵𝐵 ≈ 1o ) → { 𝐴 } ≈ 𝐵 )
14 fisseneq ( ( 𝐵 ∈ Fin ∧ { 𝐴 } ⊆ 𝐵 ∧ { 𝐴 } ≈ 𝐵 ) → { 𝐴 } = 𝐵 )
15 7 9 13 14 syl3anc ( ( 𝐴𝐵𝐵 ≈ 1o ) → { 𝐴 } = 𝐵 )
16 15 eqcomd ( ( 𝐴𝐵𝐵 ≈ 1o ) → 𝐵 = { 𝐴 } )