omsmo

Description: A strictly monotonic ordinal function on the set of natural numbers is one-to-one. (Contributed by NM, 30-Nov-2003) (Revised by David Abernethy, 1-Jan-2014)

		Ref	Expression
	Assertion	omsmo	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to F : ω \underset{1-1}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to F : ω ⟶ A$
2		omsmolem	$⊢ z \in ω \to (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (y \in z \to F (y) \in F (z)))$
3	2	adantl	$⊢ (y \in ω \land z \in ω) \to (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (y \in z \to F (y) \in F (z)))$
4	3	imp	$⊢ ((y \in ω \land z \in ω) \land ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x))) \to (y \in z \to F (y) \in F (z))$
5		omsmolem	$⊢ y \in ω \to (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (z \in y \to F (z) \in F (y)))$
6	5	adantr	$⊢ (y \in ω \land z \in ω) \to (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (z \in y \to F (z) \in F (y)))$
7	6	imp	$⊢ ((y \in ω \land z \in ω) \land ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x))) \to (z \in y \to F (z) \in F (y))$
8	4 7	orim12d	$⊢ ((y \in ω \land z \in ω) \land ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x))) \to ((y \in z \lor z \in y) \to (F (y) \in F (z) \lor F (z) \in F (y)))$
9	8	ancoms	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land (y \in ω \land z \in ω)) \to ((y \in z \lor z \in y) \to (F (y) \in F (z) \lor F (z) \in F (y)))$
10	9	con3d	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land (y \in ω \land z \in ω)) \to (\neg (F (y) \in F (z) \lor F (z) \in F (y)) \to \neg (y \in z \lor z \in y))$
11		ffvelrn	$⊢ (F : ω ⟶ A \land y \in ω) \to F (y) \in A$
12		ssel	$⊢ A \subseteq On \to (F (y) \in A \to F (y) \in On)$
13	11 12	syl5	$⊢ A \subseteq On \to ((F : ω ⟶ A \land y \in ω) \to F (y) \in On)$
14	13	expdimp	$⊢ (A \subseteq On \land F : ω ⟶ A) \to (y \in ω \to F (y) \in On)$
15		eloni	$⊢ F (y) \in On \to Ord F (y)$
16	14 15	syl6	$⊢ (A \subseteq On \land F : ω ⟶ A) \to (y \in ω \to Ord F (y))$
17		ffvelrn	$⊢ (F : ω ⟶ A \land z \in ω) \to F (z) \in A$
18		ssel	$⊢ A \subseteq On \to (F (z) \in A \to F (z) \in On)$
19	17 18	syl5	$⊢ A \subseteq On \to ((F : ω ⟶ A \land z \in ω) \to F (z) \in On)$
20	19	expdimp	$⊢ (A \subseteq On \land F : ω ⟶ A) \to (z \in ω \to F (z) \in On)$
21		eloni	$⊢ F (z) \in On \to Ord F (z)$
22	20 21	syl6	$⊢ (A \subseteq On \land F : ω ⟶ A) \to (z \in ω \to Ord F (z))$
23	16 22	anim12d	$⊢ (A \subseteq On \land F : ω ⟶ A) \to ((y \in ω \land z \in ω) \to (Ord F (y) \land Ord F (z)))$
24	23	imp	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land (y \in ω \land z \in ω)) \to (Ord F (y) \land Ord F (z))$
25		ordtri3	$⊢ (Ord F (y) \land Ord F (z)) \to (F (y) = F (z) \leftrightarrow \neg (F (y) \in F (z) \lor F (z) \in F (y)))$
26	24 25	syl	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land (y \in ω \land z \in ω)) \to (F (y) = F (z) \leftrightarrow \neg (F (y) \in F (z) \lor F (z) \in F (y)))$
27	26	adantlr	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land (y \in ω \land z \in ω)) \to (F (y) = F (z) \leftrightarrow \neg (F (y) \in F (z) \lor F (z) \in F (y)))$
28		nnord	$⊢ y \in ω \to Ord y$
29		nnord	$⊢ z \in ω \to Ord z$
30		ordtri3	$⊢ (Ord y \land Ord z) \to (y = z \leftrightarrow \neg (y \in z \lor z \in y))$
31	28 29 30	syl2an	$⊢ (y \in ω \land z \in ω) \to (y = z \leftrightarrow \neg (y \in z \lor z \in y))$
32	31	adantl	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land (y \in ω \land z \in ω)) \to (y = z \leftrightarrow \neg (y \in z \lor z \in y))$
33	10 27 32	3imtr4d	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land (y \in ω \land z \in ω)) \to (F (y) = F (z) \to y = z)$
34	33	ralrimivva	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to \forall y \in ω \forall z \in ω (F (y) = F (z) \to y = z)$
35		dff13	$⊢ F : ω \underset{1-1}{⟶} A \leftrightarrow (F : ω ⟶ A \land \forall y \in ω \forall z \in ω (F (y) = F (z) \to y = z))$
36	1 34 35	sylanbrc	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to F : ω \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem omsmo

Proof