smo11

Description: A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013)

		Ref	Expression
	Assertion	smo11	$⊢ (F : A ⟶ B \land Smo F) \to F : A \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F : A ⟶ B \land Smo F) \to F : A ⟶ B$
2		ffn	$⊢ F : A ⟶ B \to F Fn A$
3		smodm2	$⊢ (F Fn A \land Smo F) \to Ord A$
4		ordelord	$⊢ (Ord A \land z \in A) \to Ord z$
5	4	ex	$⊢ Ord A \to (z \in A \to Ord z)$
6	3 5	syl	$⊢ (F Fn A \land Smo F) \to (z \in A \to Ord z)$
7		ordelord	$⊢ (Ord A \land w \in A) \to Ord w$
8	7	ex	$⊢ Ord A \to (w \in A \to Ord w)$
9	3 8	syl	$⊢ (F Fn A \land Smo F) \to (w \in A \to Ord w)$
10	6 9	anim12d	$⊢ (F Fn A \land Smo F) \to ((z \in A \land w \in A) \to (Ord z \land Ord w))$
11		ordtri3or	$⊢ (Ord z \land Ord w) \to (z \in w \lor z = w \lor w \in z)$
12		simp1rr	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land z \in w \land F (z) = F (w)) \to w \in A$
13		smoel2	$⊢ ((F Fn A \land Smo F) \land (x \in A \land y \in x)) \to F (y) \in F (x)$
14	13	ralrimivva	$⊢ (F Fn A \land Smo F) \to \forall x \in A \forall y \in x F (y) \in F (x)$
15	14	adantr	$⊢ ((F Fn A \land Smo F) \land (z \in A \land w \in A)) \to \forall x \in A \forall y \in x F (y) \in F (x)$
16	15	3ad2ant1	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land z \in w \land F (z) = F (w)) \to \forall x \in A \forall y \in x F (y) \in F (x)$
17		simp2	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land z \in w \land F (z) = F (w)) \to z \in w$
18		simp3	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land z \in w \land F (z) = F (w)) \to F (z) = F (w)$
19		fveq2	$⊢ x = w \to F (x) = F (w)$
20	19	eleq2d	$⊢ x = w \to (F (y) \in F (x) \leftrightarrow F (y) \in F (w))$
21	20	raleqbi1dv	$⊢ x = w \to (\forall y \in x F (y) \in F (x) \leftrightarrow \forall y \in w F (y) \in F (w))$
22	21	rspcv	$⊢ w \in A \to (\forall x \in A \forall y \in x F (y) \in F (x) \to \forall y \in w F (y) \in F (w))$
23		fveq2	$⊢ y = z \to F (y) = F (z)$
24	23	eleq1d	$⊢ y = z \to (F (y) \in F (w) \leftrightarrow F (z) \in F (w))$
25	24	rspccv	$⊢ \forall y \in w F (y) \in F (w) \to (z \in w \to F (z) \in F (w))$
26	22 25	syl6	$⊢ w \in A \to (\forall x \in A \forall y \in x F (y) \in F (x) \to (z \in w \to F (z) \in F (w)))$
27	26	3imp	$⊢ (w \in A \land \forall x \in A \forall y \in x F (y) \in F (x) \land z \in w) \to F (z) \in F (w)$
28		eleq1	$⊢ F (z) = F (w) \to (F (z) \in F (w) \leftrightarrow F (w) \in F (w))$
29	28	biimpac	$⊢ (F (z) \in F (w) \land F (z) = F (w)) \to F (w) \in F (w)$
30	27 29	sylan	$⊢ ((w \in A \land \forall x \in A \forall y \in x F (y) \in F (x) \land z \in w) \land F (z) = F (w)) \to F (w) \in F (w)$
31	12 16 17 18 30	syl31anc	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land z \in w \land F (z) = F (w)) \to F (w) \in F (w)$
32		smofvon2	$⊢ Smo F \to F (w) \in On$
33		eloni	$⊢ F (w) \in On \to Ord F (w)$
34		ordirr	$⊢ Ord F (w) \to \neg F (w) \in F (w)$
35	32 33 34	3syl	$⊢ Smo F \to \neg F (w) \in F (w)$
36	35	ad2antlr	$⊢ ((F Fn A \land Smo F) \land (z \in A \land w \in A)) \to \neg F (w) \in F (w)$
37	36	3ad2ant1	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land z \in w \land F (z) = F (w)) \to \neg F (w) \in F (w)$
38	31 37	pm2.21dd	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land z \in w \land F (z) = F (w)) \to z = w$
39	38	3exp	$⊢ ((F Fn A \land Smo F) \land (z \in A \land w \in A)) \to (z \in w \to (F (z) = F (w) \to z = w))$
40		ax-1	$⊢ z = w \to (F (z) = F (w) \to z = w)$
41	40	a1i	$⊢ ((F Fn A \land Smo F) \land (z \in A \land w \in A)) \to (z = w \to (F (z) = F (w) \to z = w))$
42		simp1rl	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land w \in z \land F (z) = F (w)) \to z \in A$
43	15	3ad2ant1	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land w \in z \land F (z) = F (w)) \to \forall x \in A \forall y \in x F (y) \in F (x)$
44		simp2	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land w \in z \land F (z) = F (w)) \to w \in z$
45		simp3	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land w \in z \land F (z) = F (w)) \to F (z) = F (w)$
46		fveq2	$⊢ x = z \to F (x) = F (z)$
47	46	eleq2d	$⊢ x = z \to (F (y) \in F (x) \leftrightarrow F (y) \in F (z))$
48	47	raleqbi1dv	$⊢ x = z \to (\forall y \in x F (y) \in F (x) \leftrightarrow \forall y \in z F (y) \in F (z))$
49	48	rspcv	$⊢ z \in A \to (\forall x \in A \forall y \in x F (y) \in F (x) \to \forall y \in z F (y) \in F (z))$
50		fveq2	$⊢ y = w \to F (y) = F (w)$
51	50	eleq1d	$⊢ y = w \to (F (y) \in F (z) \leftrightarrow F (w) \in F (z))$
52	51	rspccv	$⊢ \forall y \in z F (y) \in F (z) \to (w \in z \to F (w) \in F (z))$
53	49 52	syl6	$⊢ z \in A \to (\forall x \in A \forall y \in x F (y) \in F (x) \to (w \in z \to F (w) \in F (z)))$
54	53	3imp	$⊢ (z \in A \land \forall x \in A \forall y \in x F (y) \in F (x) \land w \in z) \to F (w) \in F (z)$
55		eleq2	$⊢ F (z) = F (w) \to (F (w) \in F (z) \leftrightarrow F (w) \in F (w))$
56	55	biimpac	$⊢ (F (w) \in F (z) \land F (z) = F (w)) \to F (w) \in F (w)$
57	54 56	sylan	$⊢ ((z \in A \land \forall x \in A \forall y \in x F (y) \in F (x) \land w \in z) \land F (z) = F (w)) \to F (w) \in F (w)$
58	42 43 44 45 57	syl31anc	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land w \in z \land F (z) = F (w)) \to F (w) \in F (w)$
59	36	3ad2ant1	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land w \in z \land F (z) = F (w)) \to \neg F (w) \in F (w)$
60	58 59	pm2.21dd	$⊢ (((F Fn A \land Smo F) \land (z \in A \land w \in A)) \land w \in z \land F (z) = F (w)) \to z = w$
61	60	3exp	$⊢ ((F Fn A \land Smo F) \land (z \in A \land w \in A)) \to (w \in z \to (F (z) = F (w) \to z = w))$
62	39 41 61	3jaod	$⊢ ((F Fn A \land Smo F) \land (z \in A \land w \in A)) \to ((z \in w \lor z = w \lor w \in z) \to (F (z) = F (w) \to z = w))$
63	11 62	syl5	$⊢ ((F Fn A \land Smo F) \land (z \in A \land w \in A)) \to ((Ord z \land Ord w) \to (F (z) = F (w) \to z = w))$
64	63	ex	$⊢ (F Fn A \land Smo F) \to ((z \in A \land w \in A) \to ((Ord z \land Ord w) \to (F (z) = F (w) \to z = w)))$
65	10 64	mpdd	$⊢ (F Fn A \land Smo F) \to ((z \in A \land w \in A) \to (F (z) = F (w) \to z = w))$
66	65	ralrimivv	$⊢ (F Fn A \land Smo F) \to \forall z \in A \forall w \in A (F (z) = F (w) \to z = w)$
67	2 66	sylan	$⊢ (F : A ⟶ B \land Smo F) \to \forall z \in A \forall w \in A (F (z) = F (w) \to z = w)$
68		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))$
69	1 67 68	sylanbrc	$⊢ (F : A ⟶ B \land Smo F) \to F : A \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem smo11

Proof