Metamath Proof Explorer

Theorem s4dom

Description: The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dmeq	$⊢ E = ⟨“ A B C D ”⟩ \to dom E = dom ⟨“ A B C D ”⟩$
2		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⟩\}$
3	2	dmeqd	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to dom ⟨“ A B C D ”⟩ = dom (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\})$
4		dmun	$⊢ dom (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}) = dom \{⟨0, A⟩, ⟨1, B⟩\} \cup dom \{⟨2, C⟩, ⟨3, D⟩\}$
5		dmpropg	$⊢ (A \in S \land B \in S) \to dom \{⟨0, A⟩, ⟨1, B⟩\} = \{0, 1\}$
6	5	adantr	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to dom \{⟨0, A⟩, ⟨1, B⟩\} = \{0, 1\}$
7		dmpropg	$⊢ (C \in S \land D \in S) \to dom \{⟨2, C⟩, ⟨3, D⟩\} = \{2, 3\}$
8	7	adantl	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to dom \{⟨2, C⟩, ⟨3, D⟩\} = \{2, 3\}$
9	6 8	uneq12d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to dom \{⟨0, A⟩, ⟨1, B⟩\} \cup dom \{⟨2, C⟩, ⟨3, D⟩\} = \{0, 1\} \cup \{2, 3\}$
10	4 9	syl5eq	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to dom (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}) = \{0, 1\} \cup \{2, 3\}$
11	3 10	eqtrd	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to dom ⟨“ A B C D ”⟩ = \{0, 1\} \cup \{2, 3\}$
12	1 11	sylan9eqr	$⊢ (((A \in S \land B \in S) \land (C \in S \land D \in S)) \land E = ⟨“ A B C D ”⟩) \to dom E = \{0, 1\} \cup \{2, 3\}$
13	12	ex	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (E = ⟨“ A B C D ”⟩ \to dom E = \{0, 1\} \cup \{2, 3\})$