Metamath Proof Explorer

Theorem issmo2

Description: Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013)

Ref Expression
Assertion issmo2 ⊢ F : A ⟶ B → B ⊆ On ∧ Ord ⁡ A ∧ ∀ x ∈ A ∀ y ∈ x F ⁡ y ∈ F ⁡ x → Smo ⁡ F

Proof

Step Hyp Ref Expression
1 fss ⊢ F : A ⟶ B ∧ B ⊆ On → F : A ⟶ On
2 1 ex ⊢ F : A ⟶ B → B ⊆ On → F : A ⟶ On
3 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
4 3 feq2d ⊢ F : A ⟶ B → F : dom ⁡ F ⟶ On ↔ F : A ⟶ On
5 2 4 sylibrd ⊢ F : A ⟶ B → B ⊆ On → F : dom ⁡ F ⟶ On
6 ordeq ⊢ dom ⁡ F = A → Ord ⁡ dom ⁡ F ↔ Ord ⁡ A
7 3 6 syl ⊢ F : A ⟶ B → Ord ⁡ dom ⁡ F ↔ Ord ⁡ A
8 7 biimprd ⊢ F : A ⟶ B → Ord ⁡ A → Ord ⁡ dom ⁡ F
9 3 raleqdv ⊢ F : A ⟶ B → ∀ x ∈ dom ⁡ F ∀ y ∈ x F ⁡ y ∈ F ⁡ x ↔ ∀ x ∈ A ∀ y ∈ x F ⁡ y ∈ F ⁡ x
10 9 biimprd ⊢ F : A ⟶ B → ∀ x ∈ A ∀ y ∈ x F ⁡ y ∈ F ⁡ x → ∀ x ∈ dom ⁡ F ∀ y ∈ x F ⁡ y ∈ F ⁡ x
11 5 8 10 3anim123d ⊢ F : A ⟶ B → B ⊆ On ∧ Ord ⁡ A ∧ ∀ x ∈ A ∀ y ∈ x F ⁡ y ∈ F ⁡ x → F : dom ⁡ F ⟶ On ∧ Ord ⁡ dom ⁡ F ∧ ∀ x ∈ dom ⁡ F ∀ y ∈ x F ⁡ y ∈ F ⁡ x
12 dfsmo2 ⊢ Smo ⁡ F ↔ F : dom ⁡ F ⟶ On ∧ Ord ⁡ dom ⁡ F ∧ ∀ x ∈ dom ⁡ F ∀ y ∈ x F ⁡ y ∈ F ⁡ x
13 11 12 imbitrrdi ⊢ F : A ⟶ B → B ⊆ On ∧ Ord ⁡ A ∧ ∀ x ∈ A ∀ y ∈ x F ⁡ y ∈ F ⁡ x → Smo ⁡ F