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→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) ) )