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

Metamath Proof Explorer

Theorem s3tpop

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

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

Proof

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