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 ⊢ 𝐴 : 𝐵 ⟶ On
issmo.2 ⊢ Ord 𝐵
issmo.3 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
issmo.4 ⊢ dom 𝐴 = 𝐵
Assertion issmo Smo 𝐴

Proof

Step Hyp Ref Expression
1 issmo.1 ⊢ 𝐴 : 𝐵 ⟶ On
2 issmo.2 ⊢ Ord 𝐵
3 issmo.3 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
4 issmo.4 ⊢ dom 𝐴 = 𝐵
5 4 feq2i ⊢ ( 𝐴 : dom 𝐴 ⟶ On ↔ 𝐴 : 𝐵 ⟶ On )
6 1 5 mpbir ⊢ 𝐴 : dom 𝐴 ⟶ On
7 ordeq ⊢ ( dom 𝐴 = 𝐵 → ( Ord dom 𝐴 ↔ Ord 𝐵 ) )
8 4 7 ax-mp ⊢ ( Ord dom 𝐴 ↔ Ord 𝐵 )
9 2 8 mpbir ⊢ Ord dom 𝐴
10 4 eleq2i ⊢ ( 𝑥 ∈ dom 𝐴 ↔ 𝑥 ∈ 𝐵 )
11 4 eleq2i ⊢ ( 𝑦 ∈ dom 𝐴 ↔ 𝑦 ∈ 𝐵 )
12 10 11 3 syl2anb ⊢ ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
13 12 rgen2 ⊢ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) )
14 df-smo ⊢ ( Smo 𝐴 ↔ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
15 6 9 13 14 mpbir3an ⊢ Smo 𝐴