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

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

Metamath Proof Explorer