onelfvnef1

Description: A sufficient condition for a function on ordinals to be one-to-one. (Contributed by NM, 9-Feb-1997) Extract from tz7.48lem and generalize statement. (Revised by Matthew House, 6-Sep-2026)

		Ref	Expression
	Assertion	onelfvnef1	$⊢ (F : A ⟶ B \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y))) \to F : A \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F : A ⟶ B \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y))) \to F : A ⟶ B$
2		elequ12	$⊢ (y = z \land x = w) \to (y \in x \leftrightarrow z \in w)$
3	2	ancoms	$⊢ (x = w \land y = z) \to (y \in x \leftrightarrow z \in w)$
4		fveq2	$⊢ x = w \to F (x) = F (w)$
5		fveq2	$⊢ y = z \to F (y) = F (z)$
6	4 5	eqeqan12d	$⊢ (x = w \land y = z) \to (F (x) = F (y) \leftrightarrow F (w) = F (z))$
7	6	necon3bid	$⊢ (x = w \land y = z) \to (F (x) \neq F (y) \leftrightarrow F (w) \neq F (z))$
8	3 7	imbi12d	$⊢ (x = w \land y = z) \to ((y \in x \to F (x) \neq F (y)) \leftrightarrow (z \in w \to F (w) \neq F (z)))$
9	8	rspc2gv	$⊢ (w \in A \land z \in A) \to (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \to (z \in w \to F (w) \neq F (z)))$
10	9	ancoms	$⊢ (z \in A \land w \in A) \to (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \to (z \in w \to F (w) \neq F (z)))$
11	10	impcom	$⊢ (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \land (z \in A \land w \in A)) \to (z \in w \to F (w) \neq F (z))$
12		necom	$⊢ F (z) \neq F (w) \leftrightarrow F (w) \neq F (z)$
13	11 12	imbitrrdi	$⊢ (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \land (z \in A \land w \in A)) \to (z \in w \to F (z) \neq F (w))$
14		elequ12	$⊢ (y = w \land x = z) \to (y \in x \leftrightarrow w \in z)$
15	14	ancoms	$⊢ (x = z \land y = w) \to (y \in x \leftrightarrow w \in z)$
16		fveq2	$⊢ x = z \to F (x) = F (z)$
17		fveq2	$⊢ y = w \to F (y) = F (w)$
18	16 17	eqeqan12d	$⊢ (x = z \land y = w) \to (F (x) = F (y) \leftrightarrow F (z) = F (w))$
19	18	necon3bid	$⊢ (x = z \land y = w) \to (F (x) \neq F (y) \leftrightarrow F (z) \neq F (w))$
20	15 19	imbi12d	$⊢ (x = z \land y = w) \to ((y \in x \to F (x) \neq F (y)) \leftrightarrow (w \in z \to F (z) \neq F (w)))$
21	20	rspc2gv	$⊢ (z \in A \land w \in A) \to (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \to (w \in z \to F (z) \neq F (w)))$
22	21	impcom	$⊢ (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \land (z \in A \land w \in A)) \to (w \in z \to F (z) \neq F (w))$
23	13 22	jaod	$⊢ (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \land (z \in A \land w \in A)) \to ((z \in w \lor w \in z) \to F (z) \neq F (w))$
24	23	necon2bd	$⊢ (\forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y)) \land (z \in A \land w \in A)) \to (F (z) = F (w) \to \neg (z \in w \lor w \in z))$
25	24	3ad2antl3	$⊢ ((F : A ⟶ B \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y))) \land (z \in A \land w \in A)) \to (F (z) = F (w) \to \neg (z \in w \lor w \in z))$
26		ssel2	$⊢ (A \subseteq On \land z \in A) \to z \in On$
27		ssel2	$⊢ (A \subseteq On \land w \in A) \to w \in On$
28		eloni	$⊢ z \in On \to Ord z$
29		eloni	$⊢ w \in On \to Ord w$
30		ordtri3	$⊢ (Ord z \land Ord w) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
31	28 29 30	syl2an	$⊢ (z \in On \land w \in On) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
32	26 27 31	syl2an	$⊢ ((A \subseteq On \land z \in A) \land (A \subseteq On \land w \in A)) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
33	32	anandis	$⊢ (A \subseteq On \land (z \in A \land w \in A)) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
34	33	3ad2antl2	$⊢ ((F : A ⟶ B \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y))) \land (z \in A \land w \in A)) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
35	25 34	sylibrd	$⊢ ((F : A ⟶ B \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y))) \land (z \in A \land w \in A)) \to (F (z) = F (w) \to z = w)$
36	35	ralrimivva	$⊢ (F : A ⟶ B \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y))) \to \forall z \in A \forall w \in A (F (z) = F (w) \to z = w)$
37		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall z \in A \forall w \in A (F (z) = F (w) \to z = w))$
38	1 36 37	sylanbrc	$⊢ (F : A ⟶ B \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to F (x) \neq F (y))) \to F : A \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem onelfvnef1

Proof