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	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“AB”⟩=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-s2	$$⊢⟨“AB”⟩=⟨“A”⟩\mathrm{++}⟨“B”⟩$$
2		s1cl	$$⊢A\in S\to ⟨“A”⟩\in \mathrm{Word}S$$
3		cats1un	$$⊢\left(⟨“A”⟩\in \mathrm{Word}S\wedge B\in S\right)\to ⟨“A”⟩\mathrm{++}⟨“B”⟩=⟨“A”⟩\cup \left\{⟨\left|⟨“A”⟩\right|,B⟩\right\}$$
4	2 3	sylan	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“A”⟩\mathrm{++}⟨“B”⟩=⟨“A”⟩\cup \left\{⟨\left|⟨“A”⟩\right|,B⟩\right\}$$
5		s1val	$$⊢A\in S\to ⟨“A”⟩=\left\{⟨0,A⟩\right\}$$
6	5	adantr	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“A”⟩=\left\{⟨0,A⟩\right\}$$
7	6	uneq1d	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“A”⟩\cup \left\{⟨\left|⟨“A”⟩\right|,B⟩\right\}=\left\{⟨0,A⟩\right\}\cup \left\{⟨\left|⟨“A”⟩\right|,B⟩\right\}$$
8		df-pr	$$⊢\left\{⟨0,A⟩,⟨\left|⟨“A”⟩\right|,B⟩\right\}=\left\{⟨0,A⟩\right\}\cup \left\{⟨\left|⟨“A”⟩\right|,B⟩\right\}$$
9		s1len	$$⊢\left|⟨“A”⟩\right|=1$$
10	9	a1i	$$⊢\left(A\in S\wedge B\in S\right)\to \left|⟨“A”⟩\right|=1$$
11	10	opeq1d	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨\left|⟨“A”⟩\right|,B⟩=⟨1,B⟩$$
12	11	preq2d	$$⊢\left(A\in S\wedge B\in S\right)\to \left\{⟨0,A⟩,⟨\left|⟨“A”⟩\right|,B⟩\right\}=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$
13	8 12	eqtr3id	$$⊢\left(A\in S\wedge B\in S\right)\to \left\{⟨0,A⟩\right\}\cup \left\{⟨\left|⟨“A”⟩\right|,B⟩\right\}=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$
14	4 7 13	3eqtrd	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“A”⟩\mathrm{++}⟨“B”⟩=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$
15	1 14	syl5eq	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“AB”⟩=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$