Theorem s2prop

Description: A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017)

	Ref	Expression
Assertion	s2prop	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		df-s2	⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )
2		s1cl	⊢ ( 𝐴 ∈ 𝑆 → ⟨“ 𝐴 ”⟩ ∈ Word 𝑆 )
3		cats1un	⊢ ( ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = ( ⟨“ 𝐴 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) )
4	2 3	sylan	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = ( ⟨“ 𝐴 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) )
5		s1val	⊢ ( 𝐴 ∈ 𝑆 → ⟨“ 𝐴 ”⟩ = { ⟨ 0 , 𝐴 ⟩ } )
6	5	adantr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 ”⟩ = { ⟨ 0 , 𝐴 ⟩ } )
7	6	uneq1d	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) )
8		df-pr	⊢ { ⟨ 0 , 𝐴 ⟩ , ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } = ( { ⟨ 0 , 𝐴 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } )
9		s1len	⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1
10	9	a1i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1 )
11	10	opeq1d	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ = ⟨ 1 , 𝐵 ⟩ )
12	11	preq2d	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
13	8 12	eqtr3id	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( { ⟨ 0 , 𝐴 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
14	4 7 13	3eqtrd	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
15	1 14	syl5eq	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )