s4prop

Description: A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017)

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

Proof

Step	Hyp	Ref	Expression
1		df-s4	$⊢ ⟨“ A B C D ”⟩ = ⟨“ A B C ”⟩ ++ ⟨“ D ”⟩$
2		simpl	$⊢ (A \in S \land B \in S) \to A \in S$
3	2	adantr	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to A \in S$
4		simpr	$⊢ (A \in S \land B \in S) \to B \in S$
5	4	adantr	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to B \in S$
6		simpl	$⊢ (C \in S \land D \in S) \to C \in S$
7	6	adantl	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to C \in S$
8	3 5 7	s3cld	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C ”⟩ \in Word S$
9		simpr	$⊢ (C \in S \land D \in S) \to D \in S$
10	9	adantl	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to D \in S$
11		cats1un	$⊢ (⟨“ A B C ”⟩ \in Word S \land D \in S) \to ⟨“ A B C ”⟩ ++ ⟨“ D ”⟩ = ⟨“ A B C ”⟩ \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\}$
12	8 10 11	syl2anc	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C ”⟩ ++ ⟨“ D ”⟩ = ⟨“ A B C ”⟩ \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\}$
13		df-s3	$⊢ ⟨“ A B C ”⟩ = ⟨“ A B ”⟩ ++ ⟨“ C ”⟩$
14		s2cl	$⊢ (A \in S \land B \in S) \to ⟨“ A B ”⟩ \in Word S$
15	14	adantr	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B ”⟩ \in Word S$
16		cats1un	$⊢ (⟨“ A B ”⟩ \in Word S \land C \in S) \to ⟨“ A B ”⟩ ++ ⟨“ C ”⟩ = ⟨“ A B ”⟩ \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}$
17	15 7 16	syl2anc	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B ”⟩ ++ ⟨“ C ”⟩ = ⟨“ A B ”⟩ \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}$
18	13 17	syl5eq	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C ”⟩ = ⟨“ A B ”⟩ \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}$
19		s2prop	$⊢ (A \in S \land B \in S) \to ⟨“ A B ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\}$
20	19	adantr	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\}$
21	20	uneq1d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B ”⟩ \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\} = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}$
22	18 21	eqtrd	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}$
23	22	uneq1d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C ”⟩ \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\} = (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}) \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\}$
24	12 23	eqtrd	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C ”⟩ ++ ⟨“ D ”⟩ = (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}) \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\}$
25		unass	$⊢ (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}) \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\} = \{⟨0, A⟩, ⟨1, B⟩\} \cup (\{⟨\|⟨“ A B ”⟩\|, C⟩\} \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\})$
26	25	a1i	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨\|⟨“ A B ”⟩\|, C⟩\}) \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\} = \{⟨0, A⟩, ⟨1, B⟩\} \cup (\{⟨\|⟨“ A B ”⟩\|, C⟩\} \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\})$
27		df-pr	$⊢ \{⟨\|⟨“ A B ”⟩\|, C⟩, ⟨\|⟨“ A B C ”⟩\|, D⟩\} = \{⟨\|⟨“ A B ”⟩\|, C⟩\} \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\}$
28		s2len	$⊢ \|⟨“ A B ”⟩\| = 2$
29	28	a1i	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to \|⟨“ A B ”⟩\| = 2$
30	29	opeq1d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨\|⟨“ A B ”⟩\|, C⟩ = ⟨2, C⟩$
31		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
32	31	a1i	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to \|⟨“ A B C ”⟩\| = 3$
33	32	opeq1d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨\|⟨“ A B C ”⟩\|, D⟩ = ⟨3, D⟩$
34	30 33	preq12d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to \{⟨\|⟨“ A B ”⟩\|, C⟩, ⟨\|⟨“ A B C ”⟩\|, D⟩\} = \{⟨2, C⟩, ⟨3, D⟩\}$
35	27 34	syl5eqr	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to \{⟨\|⟨“ A B ”⟩\|, C⟩\} \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\} = \{⟨2, C⟩, ⟨3, D⟩\}$
36	35	uneq2d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to \{⟨0, A⟩, ⟨1, B⟩\} \cup (\{⟨\|⟨“ A B ”⟩\|, C⟩\} \cup \{⟨\|⟨“ A B C ”⟩\|, D⟩\}) = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}$
37	24 26 36	3eqtrd	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C ”⟩ ++ ⟨“ D ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}$
38	1 37	syl5eq	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C D ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}$

Metamath Proof Explorer

Theorem s4prop

Proof