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	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D)) \to (E = ⟨“ A B C D ”⟩ \to E : dom E \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\}))$

Proof

Step	Hyp	Ref	Expression
1		f1oun2prg	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D)) \to (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}) : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\})$
2	1	imp	$⊢ (((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \to (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}) : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\}$
3	2	adantr	$⊢ ((((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \land E = ⟨“ A B C D ”⟩) \to (\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}) : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\}$
4		s4prop	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨“ A B C D ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}$
5	4	adantr	$⊢ (((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \to ⟨“ A B C D ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}$
6	5	eqeq2d	$⊢ (((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \to (E = ⟨“ A B C D ”⟩ \leftrightarrow E = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\})$
7	6	biimpa	$⊢ ((((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \land E = ⟨“ A B C D ”⟩) \to E = \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}$
8	7	eqcomd	$⊢ ((((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \land E = ⟨“ A B C D ”⟩) \to \{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\} = E$
9	8	f1oeq1d	$⊢ ((((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \land E = ⟨“ A B C D ”⟩) \to ((\{⟨0, A⟩, ⟨1, B⟩\} \cup \{⟨2, C⟩, ⟨3, D⟩\}) : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\} \leftrightarrow E : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\})$
10	3 9	mpbid	$⊢ ((((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \land E = ⟨“ A B C D ”⟩) \to E : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\}$
11		dff1o5	$⊢ E : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\} \leftrightarrow (E : \{0, 1\} \cup \{2, 3\} \underset{1-1}{⟶} \{A, B\} \cup \{C, D\} \land ran E = \{A, B\} \cup \{C, D\})$
12		dff12	$⊢ E : \{0, 1\} \cup \{2, 3\} \underset{1-1}{⟶} \{A, B\} \cup \{C, D\} \leftrightarrow (E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{*} x x E y)$
13	12	bicomi	$⊢ (E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{*} x x E y) \leftrightarrow E : \{0, 1\} \cup \{2, 3\} \underset{1-1}{⟶} \{A, B\} \cup \{C, D\}$
14	13	anbi1i	$⊢ ((E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{*} x x E y) \land ran E = \{A, B\} \cup \{C, D\}) \leftrightarrow (E : \{0, 1\} \cup \{2, 3\} \underset{1-1}{⟶} \{A, B\} \cup \{C, D\} \land ran E = \{A, B\} \cup \{C, D\})$
15	11 14	sylbb2	$⊢ E : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\} \to ((E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{*} x x E y) \land ran E = \{A, B\} \cup \{C, D\})$
16		ffdm	$⊢ E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \to (E : dom E ⟶ \{A, B\} \cup \{C, D\} \land dom E \subseteq \{0, 1\} \cup \{2, 3\})$
17	16	simpld	$⊢ E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \to E : dom E ⟶ \{A, B\} \cup \{C, D\}$
18	17	anim1i	$⊢ (E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{} x x E y) \to (E : dom E ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{} x x E y)$
19	18	anim1i	$⊢ ((E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{} x x E y) \land ran E = \{A, B\} \cup \{C, D\}) \to ((E : dom E ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{} x x E y) \land ran E = \{A, B\} \cup \{C, D\})$
20	15 19	syl	$⊢ E : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\} \to ((E : dom E ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{*} x x E y) \land ran E = \{A, B\} \cup \{C, D\})$
21		dff12	$⊢ E : dom E \underset{1-1}{⟶} \{A, B\} \cup \{C, D\} \leftrightarrow (E : dom E ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{*} x x E y)$
22	21	anbi1i	$⊢ (E : dom E \underset{1-1}{⟶} \{A, B\} \cup \{C, D\} \land ran E = \{A, B\} \cup \{C, D\}) \leftrightarrow ((E : dom E ⟶ \{A, B\} \cup \{C, D\} \land \forall y \exists^{*} x x E y) \land ran E = \{A, B\} \cup \{C, D\})$
23	20 22	sylibr	$⊢ E : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\} \to (E : dom E \underset{1-1}{⟶} \{A, B\} \cup \{C, D\} \land ran E = \{A, B\} \cup \{C, D\})$
24		dff1o5	$⊢ E : dom E \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\} \leftrightarrow (E : dom E \underset{1-1}{⟶} \{A, B\} \cup \{C, D\} \land ran E = \{A, B\} \cup \{C, D\})$
25	23 24	sylibr	$⊢ E : \{0, 1\} \cup \{2, 3\} \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\} \to E : dom E \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\}$
26	10 25	syl	$⊢ ((((A \in S \land B \in S) \land (C \in S \land D \in S)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D))) \land E = ⟨“ A B C D ”⟩) \to E : dom E \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\}$
27	26	exp31	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D \land C \neq D)) \to (E = ⟨“ A B C D ”⟩ \to E : dom E \underset{1-1 onto}{⟶} \{A, B\} \cup \{C, D\}))$

Metamath Proof Explorer

Theorem s4f1o

Proof