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 𝐴