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	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ → dom 𝐸 = ( { 0 , 1 } ∪ { 2 , 3 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmeq	⊢ ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ → dom 𝐸 = dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ )
2		s4prop	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )
3	2	dmeqd	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = dom ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )
4		dmun	⊢ dom ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) = ( dom { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ dom { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } )
5		dmpropg	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → dom { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } = { 0 , 1 } )
6	5	adantr	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → dom { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } = { 0 , 1 } )
7		dmpropg	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → dom { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } = { 2 , 3 } )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → dom { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } = { 2 , 3 } )
9	6 8	uneq12d	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( dom { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ dom { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) = ( { 0 , 1 } ∪ { 2 , 3 } ) )
10	4 9	syl5eq	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → dom ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) = ( { 0 , 1 } ∪ { 2 , 3 } ) )
11	3 10	eqtrd	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( { 0 , 1 } ∪ { 2 , 3 } ) )
12	1 11	sylan9eqr	⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → dom 𝐸 = ( { 0 , 1 } ∪ { 2 , 3 } ) )
13	12	ex	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ → dom 𝐸 = ( { 0 , 1 } ∪ { 2 , 3 } ) ) )