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	$$⊢\phi \to I\in D$$
	s2f1.j	$$⊢\phi \to J\in D$$
	s2f1.1	$$⊢\phi \to I\ne J$$
Assertion	s2f1	$$⊢\phi \to ⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D$$

Proof

Step	Hyp	Ref	Expression
1		s2f1.i	$$⊢\phi \to I\in D$$
2		s2f1.j	$$⊢\phi \to J\in D$$
3		s2f1.1	$$⊢\phi \to I\ne J$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5	4	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7	6	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
8		0ne1	$$⊢0\ne 1$$
9	8	a1i	$$⊢\phi \to 0\ne 1$$
10		f1oprg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge I\in D\right)\wedge \left(1\in {\mathbb{N}}_0\wedge J\in D\right)\right)\to \left(\left(0\ne 1\wedge I\ne J\right)\to \left\{⟨0,I⟩,⟨1,J⟩\right\}:\left\{0,1\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}\right)$$
11	10	3impia	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge I\in D\right)\wedge \left(1\in {\mathbb{N}}_0\wedge J\in D\right)\wedge \left(0\ne 1\wedge I\ne J\right)\right)\to \left\{⟨0,I⟩,⟨1,J⟩\right\}:\left\{0,1\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
12	5 1 7 2 9 3 11	syl222anc	$$⊢\phi \to \left\{⟨0,I⟩,⟨1,J⟩\right\}:\left\{0,1\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
13		s2prop	$$⊢\left(I\in D\wedge J\in D\right)\to ⟨“IJ”⟩=\left\{⟨0,I⟩,⟨1,J⟩\right\}$$
14	1 2 13	syl2anc	$$⊢\phi \to ⟨“IJ”⟩=\left\{⟨0,I⟩,⟨1,J⟩\right\}$$
15	14	f1oeq1d	$$⊢\phi \to \left(⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}\leftrightarrow \left\{⟨0,I⟩,⟨1,J⟩\right\}:\left\{0,1\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}\right)$$
16	12 15	mpbird	$$⊢\phi \to ⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
17		f1of1	$$⊢⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}\to ⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}\left\{I,J\right\}$$
18	16 17	syl	$$⊢\phi \to ⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}\left\{I,J\right\}$$
19	1 2	prssd	$$⊢\phi \to \left\{I,J\right\}\subseteq D$$
20		f1ss	$$⊢\left(⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}\left\{I,J\right\}\wedge \left\{I,J\right\}\subseteq D\right)\to ⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}D$$
21	18 19 20	syl2anc	$$⊢\phi \to ⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}D$$
22		f1dm	$$⊢⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}D\to \mathrm{dom}⟨“IJ”⟩=\left\{0,1\right\}$$
23	21 22	syl	$$⊢\phi \to \mathrm{dom}⟨“IJ”⟩=\left\{0,1\right\}$$
24		f1eq2	$$⊢\mathrm{dom}⟨“IJ”⟩=\left\{0,1\right\}\to \left(⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D\leftrightarrow ⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}D\right)$$
25	23 24	syl	$$⊢\phi \to \left(⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D\leftrightarrow ⟨“IJ”⟩:\left\{0,1\right\}\underset{1-1}{⟶}D\right)$$
26	21 25	mpbird	$$⊢\phi \to ⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D$$