Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 df-s4 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )
2 simpl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
3 2 adantr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝐴 ∈ 𝑆 )
4 simpr ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝐵 ∈ 𝑆 )
6 simpl ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → 𝐶 ∈ 𝑆 )
7 6 adantl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝐶 ∈ 𝑆 )
8 3 5 7 s3cld ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑆 )
9 simpr ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → 𝐷 ∈ 𝑆 )
10 9 adantl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝐷 ∈ 𝑆 )
11 cats1un ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) )
12 8 10 11 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) )
13 df-s3 ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )
14 s2cl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑆 )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑆 )
16 cats1un ⊢ ( ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ ) = ( ⟨“ 𝐴 𝐵 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) )
17 15 7 16 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ ) = ( ⟨“ 𝐴 𝐵 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) )
18 13 17 syl5eq ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) )
19 s2prop ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
20 19 adantr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
21 20 uneq1d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) )
22 18 21 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) )
23 22 uneq1d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) = ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) )
24 12 23 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) = ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) )
25 unass ⊢ ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ ( { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) )
26 25 a1i ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ ( { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) ) )
27 df-pr ⊢ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ , ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } = ( { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } )
28 s2len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2
29 28 a1i ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2 )
30 29 opeq1d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ = ⟨ 2 , 𝐶 ⟩ )
31 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
32 31 a1i ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 )
33 32 opeq1d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ = ⟨ 3 , 𝐷 ⟩ )
34 30 33 preq12d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ , ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } = { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } )
35 27 34 syl5eqr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) = { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } )
36 35 uneq2d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ ( { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) , 𝐷 ⟩ } ) ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )
37 24 26 36 3eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )
38 1 37 syl5eq ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )