This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem en1b

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015) Avoid ax-un . (Revised by BTernaryTau, 24-Sep-2024)

Ref Expression
Assertion en1b ( 𝐴 ≈ 1o ↔ 𝐴 = { ∪ 𝐴 } )

Proof

Step Hyp Ref Expression
1 en1 ⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
2 id ⊢ ( 𝐴 = { 𝑥 } → 𝐴 = { 𝑥 } )
3 unieq ⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = ∪ { 𝑥 } )
4 unisnv ⊢ ∪ { 𝑥 } = 𝑥
5 3 4 eqtrdi ⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = 𝑥 )
6 5 sneqd ⊢ ( 𝐴 = { 𝑥 } → { ∪ 𝐴 } = { 𝑥 } )
7 2 6 eqtr4d ⊢ ( 𝐴 = { 𝑥 } → 𝐴 = { ∪ 𝐴 } )
8 7 exlimiv ⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐴 = { ∪ 𝐴 } )
9 1 8 sylbi ⊢ ( 𝐴 ≈ 1o → 𝐴 = { ∪ 𝐴 } )
10 id ⊢ ( 𝐴 = { ∪ 𝐴 } → 𝐴 = { ∪ 𝐴 } )
11 eqsnuniex ⊢ ( 𝐴 = { ∪ 𝐴 } → ∪ 𝐴 ∈ V )
12 ensn1g ⊢ ( ∪ 𝐴 ∈ V → { ∪ 𝐴 } ≈ 1o )
13 11 12 syl ⊢ ( 𝐴 = { ∪ 𝐴 } → { ∪ 𝐴 } ≈ 1o )
14 10 13 eqbrtrd ⊢ ( 𝐴 = { ∪ 𝐴 } → 𝐴 ≈ 1o )
15 9 14 impbii ⊢ ( 𝐴 ≈ 1o ↔ 𝐴 = { ∪ 𝐴 } )