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