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

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 ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ → 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 eqtrid ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 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 } ) ) )