Theorem s3tpop

Description: A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021)

	Ref	Expression
Assertion	s3tpop	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to ⟨“ABC”⟩=\left\{⟨0,A⟩,⟨1,B⟩,⟨2,C⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-s3	$$⊢⟨“ABC”⟩=⟨“AB”⟩\mathrm{++}⟨“C”⟩$$
2		s2cl	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“AB”⟩\in \mathrm{Word}S$$
3		cats1un	$$⊢\left(⟨“AB”⟩\in \mathrm{Word}S\wedge C\in S\right)\to ⟨“AB”⟩\mathrm{++}⟨“C”⟩=⟨“AB”⟩\cup \left\{⟨\left|⟨“AB”⟩\right|,C⟩\right\}$$
4	2 3	stoic3	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to ⟨“AB”⟩\mathrm{++}⟨“C”⟩=⟨“AB”⟩\cup \left\{⟨\left|⟨“AB”⟩\right|,C⟩\right\}$$
5		s2prop	$$⊢\left(A\in S\wedge B\in S\right)\to ⟨“AB”⟩=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$
6	5	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to ⟨“AB”⟩=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$
7		s2len	$$⊢\left|⟨“AB”⟩\right|=2$$
8	7	opeq1i	$$⊢⟨\left|⟨“AB”⟩\right|,C⟩=⟨2,C⟩$$
9	8	sneqi	$$⊢\left\{⟨\left|⟨“AB”⟩\right|,C⟩\right\}=\left\{⟨2,C⟩\right\}$$
10	9	a1i	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to \left\{⟨\left|⟨“AB”⟩\right|,C⟩\right\}=\left\{⟨2,C⟩\right\}$$
11	6 10	uneq12d	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to ⟨“AB”⟩\cup \left\{⟨\left|⟨“AB”⟩\right|,C⟩\right\}=\left\{⟨0,A⟩,⟨1,B⟩\right\}\cup \left\{⟨2,C⟩\right\}$$
12		df-tp	$$⊢\left\{⟨0,A⟩,⟨1,B⟩,⟨2,C⟩\right\}=\left\{⟨0,A⟩,⟨1,B⟩\right\}\cup \left\{⟨2,C⟩\right\}$$
13	12	eqcomi	$$⊢\left\{⟨0,A⟩,⟨1,B⟩\right\}\cup \left\{⟨2,C⟩\right\}=\left\{⟨0,A⟩,⟨1,B⟩,⟨2,C⟩\right\}$$
14	13	a1i	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to \left\{⟨0,A⟩,⟨1,B⟩\right\}\cup \left\{⟨2,C⟩\right\}=\left\{⟨0,A⟩,⟨1,B⟩,⟨2,C⟩\right\}$$
15	4 11 14	3eqtrd	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to ⟨“AB”⟩\mathrm{++}⟨“C”⟩=\left\{⟨0,A⟩,⟨1,B⟩,⟨2,C⟩\right\}$$
16	1 15	syl5eq	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to ⟨“ABC”⟩=\left\{⟨0,A⟩,⟨1,B⟩,⟨2,C⟩\right\}$$