s2f1o

Description: A length 2 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	s2f1o	$⊢ (A \in S \land B \in S \land A \neq B) \to (E = ⟨“ A B ”⟩ \to E : \{0, 1\} \underset{1-1 onto}{⟶} \{A, B\})$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to A \in S$
2		0z	$⊢ 0 \in ℤ$
3	1 2	jctil	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to (0 \in ℤ \land A \in S)$
4		simpl2	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to B \in S$
5		1z	$⊢ 1 \in ℤ$
6	4 5	jctil	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to (1 \in ℤ \land B \in S)$
7	3 6	jca	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to ((0 \in ℤ \land A \in S) \land (1 \in ℤ \land B \in S))$
8		simpl3	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to A \neq B$
9		0ne1	$⊢ 0 \neq 1$
10	8 9	jctil	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to (0 \neq 1 \land A \neq B)$
11		f1oprg	$⊢ ((0 \in ℤ \land A \in S) \land (1 \in ℤ \land B \in S)) \to ((0 \neq 1 \land A \neq B) \to \{⟨0, A⟩, ⟨1, B⟩\} : \{0, 1\} \underset{1-1 onto}{⟶} \{A, B\})$
12	7 10 11	sylc	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to \{⟨0, A⟩, ⟨1, B⟩\} : \{0, 1\} \underset{1-1 onto}{⟶} \{A, B\}$
13		eqcom	$⊢ E = ⟨“ A B ”⟩ \leftrightarrow ⟨“ A B ”⟩ = E$
14		s2prop	$⊢ (A \in S \land B \in S) \to ⟨“ A B ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\}$
15	14	3adant3	$⊢ (A \in S \land B \in S \land A \neq B) \to ⟨“ A B ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\}$
16	15	eqeq1d	$⊢ (A \in S \land B \in S \land A \neq B) \to (⟨“ A B ”⟩ = E \leftrightarrow \{⟨0, A⟩, ⟨1, B⟩\} = E)$
17	13 16	syl5bb	$⊢ (A \in S \land B \in S \land A \neq B) \to (E = ⟨“ A B ”⟩ \leftrightarrow \{⟨0, A⟩, ⟨1, B⟩\} = E)$
18	17	biimpa	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to \{⟨0, A⟩, ⟨1, B⟩\} = E$
19		eqidd	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to \{0, 1\} = \{0, 1\}$
20		eqidd	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to \{A, B\} = \{A, B\}$
21	18 19 20	f1oeq123d	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to (\{⟨0, A⟩, ⟨1, B⟩\} : \{0, 1\} \underset{1-1 onto}{⟶} \{A, B\} \leftrightarrow E : \{0, 1\} \underset{1-1 onto}{⟶} \{A, B\})$
22	12 21	mpbid	$⊢ ((A \in S \land B \in S \land A \neq B) \land E = ⟨“ A B ”⟩) \to E : \{0, 1\} \underset{1-1 onto}{⟶} \{A, B\}$
23	22	ex	$⊢ (A \in S \land B \in S \land A \neq B) \to (E = ⟨“ A B ”⟩ \to E : \{0, 1\} \underset{1-1 onto}{⟶} \{A, B\})$

Metamath Proof Explorer

Theorem s2f1o

Proof