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

Metamath Proof Explorer

Theorem hashen1

Description: A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019)

Ref Expression
Assertion hashen1 ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ 𝐴 ≈ 1o ) )

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 hashsng ⊢ ( ∅ ∈ V → ( ♯ ‘ { ∅ } ) = 1 )
3 1 2 ax-mp ⊢ ( ♯ ‘ { ∅ } ) = 1
4 3 eqcomi ⊢ 1 = ( ♯ ‘ { ∅ } )
5 4 a1i ⊢ ( 𝐴 ∈ 𝑉 → 1 = ( ♯ ‘ { ∅ } ) )
6 5 eqeq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) )
7 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) )
8 1nn0 ⊢ 1 ∈ ℕ0
9 3 8 eqeltri ⊢ ( ♯ ‘ { ∅ } ) ∈ ℕ0
10 hashvnfin ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ { ∅ } ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) → 𝐴 ∈ Fin ) )
11 9 10 mpan2 ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) → 𝐴 ∈ Fin ) )
12 11 imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → 𝐴 ∈ Fin )
13 snfi ⊢ { ∅ } ∈ Fin
14 hashen ⊢ ( ( 𝐴 ∈ Fin ∧ { ∅ } ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ↔ 𝐴 ≈ { ∅ } ) )
15 12 13 14 sylancl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ↔ 𝐴 ≈ { ∅ } ) )
16 7 15 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → 𝐴 ≈ { ∅ } )
17 16 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) → 𝐴 ≈ { ∅ } ) )
18 hasheni ⊢ ( 𝐴 ≈ { ∅ } → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) )
19 17 18 impbid1 ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ↔ 𝐴 ≈ { ∅ } ) )
20 df1o2 ⊢ 1o = { ∅ }
21 20 eqcomi ⊢ { ∅ } = 1o
22 21 breq2i ⊢ ( 𝐴 ≈ { ∅ } ↔ 𝐴 ≈ 1o )
23 22 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ≈ { ∅ } ↔ 𝐴 ≈ 1o ) )
24 6 19 23 3bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ 𝐴 ≈ 1o ) )