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

Metamath Proof Explorer

Theorem s1dm

Description: The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020)

Ref Expression
Assertion s1dm ⊢ dom ⁡ ⟨“ A ”⟩ = 0

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ A ”⟩ ∈ Word V
2 wrdf ⊢ ⟨“ A ”⟩ ∈ Word V → ⟨“ A ”⟩ : 0 ..^ ⟨“ A ”⟩ ⟶ V
3 1 2 ax-mp ⊢ ⟨“ A ”⟩ : 0 ..^ ⟨“ A ”⟩ ⟶ V
4 s1len ⊢ ⟨“ A ”⟩ = 1
5 oveq2 ⊢ ⟨“ A ”⟩ = 1 → 0 ..^ ⟨“ A ”⟩ = 0 ..^ 1
6 fzo01 ⊢ 0 ..^ 1 = 0
7 5 6 eqtrdi ⊢ ⟨“ A ”⟩ = 1 → 0 ..^ ⟨“ A ”⟩ = 0
8 4 7 ax-mp ⊢ 0 ..^ ⟨“ A ”⟩ = 0
9 8 eqcomi ⊢ 0 = 0 ..^ ⟨“ A ”⟩
10 9 feq2i ⊢ ⟨“ A ”⟩ : 0 ⟶ V ↔ ⟨“ A ”⟩ : 0 ..^ ⟨“ A ”⟩ ⟶ V
11 3 10 mpbir ⊢ ⟨“ A ”⟩ : 0 ⟶ V
12 11 fdmi ⊢ dom ⁡ ⟨“ A ”⟩ = 0