Metamath Proof Explorer

Theorem 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 ∧ B ⊆ On → F : A ⟶ onto B ∧ Smo ⁡ F ↔ F Isom E , E A B

Proof

Step Hyp Ref Expression
1 fof ⊢ F : A ⟶ onto B → F : A ⟶ B
2 smo11 ⊢ F : A ⟶ B ∧ Smo ⁡ F → F : A ⟶ 1-1 B
3 1 2 sylan ⊢ F : A ⟶ onto B ∧ Smo ⁡ F → F : A ⟶ 1-1 B
4 simpl ⊢ F : A ⟶ onto B ∧ Smo ⁡ F → F : A ⟶ onto B
5 df-f1o ⊢ F : A ⟶ 1-1 onto B ↔ F : A ⟶ 1-1 B ∧ F : A ⟶ onto B
6 3 4 5 sylanbrc ⊢ F : A ⟶ onto B ∧ Smo ⁡ F → F : A ⟶ 1-1 onto B
7 6 adantl ⊢ Ord ⁡ A ∧ B ⊆ On ∧ F : A ⟶ onto B ∧ Smo ⁡ F → F : A ⟶ 1-1 onto B
8 fofn ⊢ F : A ⟶ onto B → F Fn A
9 smoord ⊢ F Fn A ∧ Smo ⁡ F ∧ x ∈ A ∧ y ∈ A → x ∈ y ↔ F ⁡ x ∈ F ⁡ y
10 epel ⊢ x E y ↔ x ∈ y
11 fvex ⊢ F ⁡ y ∈ V
12 11 epeli ⊢ F ⁡ x E F ⁡ y ↔ F ⁡ x ∈ F ⁡ y
13 9 10 12 3bitr4g ⊢ F Fn A ∧ Smo ⁡ F ∧ x ∈ A ∧ y ∈ A → x E y ↔ F ⁡ x E F ⁡ y
14 13 ralrimivva ⊢ F Fn A ∧ Smo ⁡ F → ∀ x ∈ A ∀ y ∈ A x E y ↔ F ⁡ x E F ⁡ y
15 8 14 sylan ⊢ F : A ⟶ onto B ∧ Smo ⁡ F → ∀ x ∈ A ∀ y ∈ A x E y ↔ F ⁡ x E F ⁡ y
16 15 adantl ⊢ Ord ⁡ A ∧ B ⊆ On ∧ F : A ⟶ onto B ∧ Smo ⁡ F → ∀ x ∈ A ∀ y ∈ A x E y ↔ F ⁡ x E F ⁡ y
17 df-isom ⊢ F Isom E , E A B ↔ F : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x E y ↔ F ⁡ x E F ⁡ y
18 7 16 17 sylanbrc ⊢ Ord ⁡ A ∧ B ⊆ On ∧ F : A ⟶ onto B ∧ Smo ⁡ F → F Isom E , E A B
19 18 ex ⊢ Ord ⁡ A ∧ B ⊆ On → F : A ⟶ onto B ∧ Smo ⁡ F → F Isom E , E A B
20 isof1o ⊢ F Isom E , E A B → F : A ⟶ 1-1 onto B
21 f1ofo ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ onto B
22 20 21 syl ⊢ F Isom E , E A B → F : A ⟶ onto B
23 22 3ad2ant1 ⊢ F Isom E , E A B ∧ Ord ⁡ A ∧ B ⊆ On → F : A ⟶ onto B
24 smoiso ⊢ F Isom E , E A B ∧ Ord ⁡ A ∧ B ⊆ On → Smo ⁡ F
25 23 24 jca ⊢ F Isom E , E A B ∧ Ord ⁡ A ∧ B ⊆ On → F : A ⟶ onto B ∧ Smo ⁡ F
26 25 3expib ⊢ F Isom E , E A B → Ord ⁡ A ∧ B ⊆ On → F : A ⟶ onto B ∧ Smo ⁡ F
27 26 com12 ⊢ Ord ⁡ A ∧ B ⊆ On → F Isom E , E A B → F : A ⟶ onto B ∧ Smo ⁡ F
28 19 27 impbid ⊢ Ord ⁡ A ∧ B ⊆ On → F : A ⟶ onto B ∧ Smo ⁡ F ↔ F Isom E , E A B