smoiso2

Description: The strictly monotone ordinal functions are also isomorphisms of subclasses of On equipped with the membership relation. (Contributed by Mario Carneiro, 20-Mar-2013)

		Ref	Expression
	Assertion	smoiso2	$⊢ (Ord A \land B \subseteq On) \to ((F : A \underset{onto}{⟶} B \land Smo F) \leftrightarrow F {Isom}_{E, E} (A, B))$

Proof

Step	Hyp	Ref	Expression
1		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
2		smo11	$⊢ (F : A ⟶ B \land Smo F) \to F : A \underset{1-1}{⟶} B$
3	1 2	sylan	$⊢ (F : A \underset{onto}{⟶} B \land Smo F) \to F : A \underset{1-1}{⟶} B$
4		simpl	$⊢ (F : A \underset{onto}{⟶} B \land Smo F) \to F : A \underset{onto}{⟶} B$
5		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
6	3 4 5	sylanbrc	$⊢ (F : A \underset{onto}{⟶} B \land Smo F) \to F : A \underset{1-1 onto}{⟶} B$
7	6	adantl	$⊢ ((Ord A \land B \subseteq On) \land (F : A \underset{onto}{⟶} B \land Smo F)) \to F : A \underset{1-1 onto}{⟶} B$
8		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
9		smoord	$⊢ ((F Fn A \land Smo F) \land (x \in A \land y \in A)) \to (x \in y \leftrightarrow F (x) \in F (y))$
10		epel	$⊢ x E y \leftrightarrow x \in y$
11		fvex	$⊢ F (y) \in V$
12	11	epeli	$⊢ F (x) E F (y) \leftrightarrow F (x) \in F (y)$
13	9 10 12	3bitr4g	$⊢ ((F Fn A \land Smo F) \land (x \in A \land y \in A)) \to (x E y \leftrightarrow F (x) E F (y))$
14	13	ralrimivva	$⊢ (F Fn A \land Smo F) \to \forall x \in A \forall y \in A (x E y \leftrightarrow F (x) E F (y))$
15	8 14	sylan	$⊢ (F : A \underset{onto}{⟶} B \land Smo F) \to \forall x \in A \forall y \in A (x E y \leftrightarrow F (x) E F (y))$
16	15	adantl	$⊢ ((Ord A \land B \subseteq On) \land (F : A \underset{onto}{⟶} B \land Smo F)) \to \forall x \in A \forall y \in A (x E y \leftrightarrow F (x) E F (y))$
17		df-isom	$⊢ F {Isom}_{E, E} (A, B) \leftrightarrow (F : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x E y \leftrightarrow F (x) E F (y)))$
18	7 16 17	sylanbrc	$⊢ ((Ord A \land B \subseteq On) \land (F : A \underset{onto}{⟶} B \land Smo F)) \to F {Isom}_{E, E} (A, B)$
19	18	ex	$⊢ (Ord A \land B \subseteq On) \to ((F : A \underset{onto}{⟶} B \land Smo F) \to F {Isom}_{E, E} (A, B))$
20		isof1o	$⊢ F {Isom}_{E, E} (A, B) \to F : A \underset{1-1 onto}{⟶} B$
21		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
22	20 21	syl	$⊢ F {Isom}_{E, E} (A, B) \to F : A \underset{onto}{⟶} B$
23	22	3ad2ant1	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to F : A \underset{onto}{⟶} B$
24		smoiso	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to Smo F$
25	23 24	jca	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to (F : A \underset{onto}{⟶} B \land Smo F)$
26	25	3expib	$⊢ F {Isom}_{E, E} (A, B) \to ((Ord A \land B \subseteq On) \to (F : A \underset{onto}{⟶} B \land Smo F))$
27	26	com12	$⊢ (Ord A \land B \subseteq On) \to (F {Isom}_{E, E} (A, B) \to (F : A \underset{onto}{⟶} B \land Smo F))$
28	19 27	impbid	$⊢ (Ord A \land B \subseteq On) \to ((F : A \underset{onto}{⟶} B \land Smo F) \leftrightarrow F {Isom}_{E, E} (A, B))$

Metamath Proof Explorer

Theorem smoiso2

Proof