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 8 f1oeq1d ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
10 3 9 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
11 dff1o5 ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
12 dff12 ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) )
13 12 bicomi ⊢ ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ↔ 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
14 13 anbi1i ⊢ ( ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ↔ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
15 11 14 sylbb2 ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
16 ffdm ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ dom 𝐸 ⊆ ( { 0 , 1 } ∪ { 2 , 3 } ) ) )
17 16 simpld ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
18 17 anim1i ⊢ ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) → ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) )
19 18 anim1i ⊢ ( ( ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) → ( ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
20 15 19 syl ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
21 dff12 ⊢ ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) )
22 21 anbi1i ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ↔ ( ( 𝐸 : dom 𝐸 ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐸 𝑦 ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
23 20 22 sylibr ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
24 dff1o5 ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ↔ ( 𝐸 : dom 𝐸 –1-1→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ∧ ran 𝐸 = ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )
25 23 24 sylibr ⊢ ( 𝐸 : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) → 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
26 10 25 syl ⊢ ( ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) → 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
27 26 exp31 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝐸 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ → 𝐸 : dom 𝐸 –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ) )