smoiso

Description: If F is an isomorphism from an ordinal A onto B , which is a subset of the ordinals, then F is a strictly monotonic function. Exercise 3 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 24-Nov-2011)

		Ref	Expression
	Assertion	smoiso	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to Smo F$

Proof

Step	Hyp	Ref	Expression
1		isof1o	$⊢ F {Isom}_{E, E} (A, B) \to F : A \underset{1-1 onto}{⟶} B$
2		f1of	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A ⟶ B$
3	1 2	syl	$⊢ F {Isom}_{E, E} (A, B) \to F : A ⟶ B$
4		ffdm	$⊢ F : A ⟶ B \to (F : dom F ⟶ B \land dom F \subseteq A)$
5	4	simpld	$⊢ F : A ⟶ B \to F : dom F ⟶ B$
6		fss	$⊢ (F : dom F ⟶ B \land B \subseteq On) \to F : dom F ⟶ On$
7	5 6	sylan	$⊢ (F : A ⟶ B \land B \subseteq On) \to F : dom F ⟶ On$
8	7	3adant2	$⊢ (F : A ⟶ B \land Ord A \land B \subseteq On) \to F : dom F ⟶ On$
9	3 8	syl3an1	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to F : dom F ⟶ On$
10		fdm	$⊢ F : A ⟶ B \to dom F = A$
11	10	eqcomd	$⊢ F : A ⟶ B \to A = dom F$
12		ordeq	$⊢ A = dom F \to (Ord A \leftrightarrow Ord dom F)$
13	1 2 11 12	4syl	$⊢ F {Isom}_{E, E} (A, B) \to (Ord A \leftrightarrow Ord dom F)$
14	13	biimpa	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A) \to Ord dom F$
15	14	3adant3	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to Ord dom F$
16	10	eleq2d	$⊢ F : A ⟶ B \to (x \in dom F \leftrightarrow x \in A)$
17	10	eleq2d	$⊢ F : A ⟶ B \to (y \in dom F \leftrightarrow y \in A)$
18	16 17	anbi12d	$⊢ F : A ⟶ B \to ((x \in dom F \land y \in dom F) \leftrightarrow (x \in A \land y \in A))$
19	1 2 18	3syl	$⊢ F {Isom}_{E, E} (A, B) \to ((x \in dom F \land y \in dom F) \leftrightarrow (x \in A \land y \in A))$
20		isorel	$⊢ (F {Isom}_{E, E} (A, B) \land (x \in A \land y \in A)) \to (x E y \leftrightarrow F (x) E F (y))$
21		epel	$⊢ x E y \leftrightarrow x \in y$
22		fvex	$⊢ F (y) \in V$
23	22	epeli	$⊢ F (x) E F (y) \leftrightarrow F (x) \in F (y)$
24	20 21 23	3bitr3g	$⊢ (F {Isom}_{E, E} (A, B) \land (x \in A \land y \in A)) \to (x \in y \leftrightarrow F (x) \in F (y))$
25	24	biimpd	$⊢ (F {Isom}_{E, E} (A, B) \land (x \in A \land y \in A)) \to (x \in y \to F (x) \in F (y))$
26	25	ex	$⊢ F {Isom}_{E, E} (A, B) \to ((x \in A \land y \in A) \to (x \in y \to F (x) \in F (y)))$
27	19 26	sylbid	$⊢ F {Isom}_{E, E} (A, B) \to ((x \in dom F \land y \in dom F) \to (x \in y \to F (x) \in F (y)))$
28	27	ralrimivv	$⊢ F {Isom}_{E, E} (A, B) \to \forall x \in dom F \forall y \in dom F (x \in y \to F (x) \in F (y))$
29	28	3ad2ant1	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to \forall x \in dom F \forall y \in dom F (x \in y \to F (x) \in F (y))$
30		df-smo	$⊢ Smo F \leftrightarrow (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in dom F (x \in y \to F (x) \in F (y)))$
31	9 15 29 30	syl3anbrc	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land B \subseteq On) \to Smo F$

Metamath Proof Explorer

Theorem smoiso

Proof