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	14	f1oeq1d	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } ↔ { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } ) )
16	12 15	mpbird	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } )
17		f1of1	⊢ ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1-onto→ { 𝐼 , 𝐽 } → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ { 𝐼 , 𝐽 } )
18	16 17	syl	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ { 𝐼 , 𝐽 } )
19	1 2	prssd	⊢ ( 𝜑 → { 𝐼 , 𝐽 } ⊆ 𝐷 )
20		f1ss	⊢ ( ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ { 𝐼 , 𝐽 } ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ) → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 )
21	18 19 20	syl2anc	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 )
22		f1dm	⊢ ( ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 → dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } )
23	21 22	syl	⊢ ( 𝜑 → dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } )
24		f1eq2	⊢ ( dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } → ( ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 ↔ ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 ) )
25	23 24	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 ↔ ⟨“ 𝐼 𝐽 ”⟩ : { 0 , 1 } –1-1→ 𝐷 ) )
26	21 25	mpbird	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )