Metamath Proof Explorer

Theorem s2f1

Description: Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses s2f1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
s2f1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
s2f1.1 ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
Assertion s2f1 ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )

Proof

Step Hyp Ref Expression
1 s2f1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
2 s2f1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
3 s2f1.1 ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
4 0nn0 ⊢ 0 ∈ ℕ0
5 4 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
6 1nn0 ⊢ 1 ∈ ℕ0
7 6 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
8 0ne1 ⊢ 0 ≠ 1
9 8 a1i ⊢ ( 𝜑 → 0 ≠ 1 )
10 f1oprg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 𝐼 ∈ 𝐷 ) ∧ ( 1 ∈ ℕ0 ∧ 𝐽 ∈ 𝐷 ) ) → ( ( 0 ≠ 1 ∧ 𝐼 ≠ 𝐽 ) → { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } ) )
11 10 3impia ⊢ ( ( ( 0 ∈ ℕ0 ∧ 𝐼 ∈ 𝐷 ) ∧ ( 1 ∈ ℕ0 ∧ 𝐽 ∈ 𝐷 ) ∧ ( 0 ≠ 1 ∧ 𝐼 ≠ 𝐽 ) ) → { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } )
12 5 1 7 2 9 3 11 syl222anc ⊢ ( 𝜑 → { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } )
13 s2prop ⊢ ( ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ) → ⟨“ 𝐼 𝐽 ”⟩ = { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } )
14 1 2 13 syl2anc ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ = { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } )
15 f1oeq1 ⊢ ( ⟨“ 𝐼 𝐽 ”⟩ = { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } → ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } ↔ { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } ) )
16 14 15 syl ⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } ↔ { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } ) )
17 12 16 mpbird ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } )
18 f1of1 ⊢ ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ { 𝐼 , 𝐽 } )
19 17 18 syl ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ { 𝐼 , 𝐽 } )
20 1 2 prssd ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ⊆ 𝐷 )
21 f1ss ⊢ ( ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ { 𝐼 , 𝐽 } ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ) → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 )
22 19 20 21 syl2anc ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 )
23 f1dm ⊢ ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 → dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } )
24 22 23 syl ⊢ ( 𝜑 → dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } )
25 f1eq2 ⊢ ( dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } → ( ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 ↔ ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 ) )
26 24 25 syl ⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 ↔ ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 ) )
27 22 26 mpbird ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )