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		eqidd	$⊢ ((((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, 1\} \cup \{2, 3\} = \{0, 1\} \cup \{2, 3\}$
10		eqidd	$⊢ ((((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 \{A, B\} \cup \{C, D\} = \{A, B\} \cup \{C, D\}$
11	8 9 10	f1oeq123d	$⊢ ((((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\})$
12	3 11	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\}$
13		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\})$
14		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)$
15	14	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\}$
16	15	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\})$
17	13 16	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\})$
18		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\})$
19	18	simpld	$⊢ E : \{0, 1\} \cup \{2, 3\} ⟶ \{A, B\} \cup \{C, D\} \to E : dom E ⟶ \{A, B\} \cup \{C, D\}$
20	19	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)$
21	20	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\})$
22	17 21	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\})$
23		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)$
24	23	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\})$
25	22 24	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\})$
26		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\})$
27	25 26	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\}$
28	12 27	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\}$
29	28	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