Metamath Proof Explorer

Theorem s4f1o

Description: A length 4 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017)

Ref Expression
Assertion s4f1o ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ → 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ) )

Proof

Step Hyp Ref Expression
1 f1oun2prg ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
2 1 imp ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
3 2 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
4 s4prop ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )
5 4 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )
6 5 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ↔ 𝐸 = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) ) )
7 6 biimpa ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → 𝐸 = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) )
8 7 eqcomd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) = 𝐸 )
9 eqidd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → ( { 0 , 1 } ∪ { 2 , 3 } ) = ( { 0 , 1 } ∪ { 2 , 3 } ) )
10 eqidd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
11 8 9 10 f1oeq123d ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
12 3 11 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
13 dff1o5 ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
14 dff12 ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) )
15 14 bicomi ⊢ ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ↔ 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
16 15 anbi1i ⊢ ( ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ↔ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
17 13 16 sylbb2 ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
18 ffdm ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ dom 𝐸 ⊆ ( { 0 , 1 } ∪ { 2 , 3 } ) ) )
19 18 simpld ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
20 19 anim1i ⊢ ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) → ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) )
21 20 anim1i ⊢ ( ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) → ( ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
22 17 21 syl ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
23 dff12 ⊢ ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) )
24 23 anbi1i ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ↔ ( ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
25 22 24 sylibr ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
26 dff1o5 ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
27 25 26 sylibr ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
28 12 27 syl ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
29 28 exp31 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ → 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ) )