This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issmo

Description: Conditions for which A is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011) Avoid ax-13 . (Revised by GG, 19-May-2023)

Ref Expression
Hypotheses issmo.1 ⊢ A : B ⟶ On
issmo.2 ⊢ Ord ⁡ B
issmo.3 ⊢ x ∈ B ∧ y ∈ B → x ∈ y → A ⁡ x ∈ A ⁡ y
issmo.4 ⊢ dom ⁡ A = B
Assertion issmo ⊢ Smo ⁡ A

Proof

Step Hyp Ref Expression
1 issmo.1 ⊢ A : B ⟶ On
2 issmo.2 ⊢ Ord ⁡ B
3 issmo.3 ⊢ x ∈ B ∧ y ∈ B → x ∈ y → A ⁡ x ∈ A ⁡ y
4 issmo.4 ⊢ dom ⁡ A = B
5 4 feq2i ⊢ A : dom ⁡ A ⟶ On ↔ A : B ⟶ On
6 1 5 mpbir ⊢ A : dom ⁡ A ⟶ On
7 ordeq ⊢ dom ⁡ A = B → Ord ⁡ dom ⁡ A ↔ Ord ⁡ B
8 4 7 ax-mp ⊢ Ord ⁡ dom ⁡ A ↔ Ord ⁡ B
9 2 8 mpbir ⊢ Ord ⁡ dom ⁡ A
10 4 eleq2i ⊢ x ∈ dom ⁡ A ↔ x ∈ B
11 4 eleq2i ⊢ y ∈ dom ⁡ A ↔ y ∈ B
12 10 11 3 syl2anb ⊢ x ∈ dom ⁡ A ∧ y ∈ dom ⁡ A → x ∈ y → A ⁡ x ∈ A ⁡ y
13 12 rgen2 ⊢ ∀ x ∈ dom ⁡ A ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y
14 df-smo ⊢ Smo ⁡ A ↔ A : dom ⁡ A ⟶ On ∧ Ord ⁡ dom ⁡ A ∧ ∀ x ∈ dom ⁡ A ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y
15 6 9 13 14 mpbir3an ⊢ Smo ⁡ A