Definition df-smo

Description: Definition of a strictly monotone ordinal function. Definition 7.46 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 15-Nov-2011)

	Ref	Expression
Assertion	df-smo	⊢ ( Smo 𝐴 ↔ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wsmo	⊢ Smo 𝐴
2	0	cdm	⊢ dom 𝐴
3		con0	⊢ On
4	2 3 0	wf	⊢ 𝐴 : dom 𝐴 ⟶ On
5	2	word	⊢ Ord dom 𝐴
6		vx	⊢ 𝑥
7		vy	⊢ 𝑦
8	6	cv	⊢ 𝑥
9	7	cv	⊢ 𝑦
10	8 9	wcel	⊢ 𝑥 ∈ 𝑦
11	8 0	cfv	⊢ ( 𝐴 ‘ 𝑥 )
12	9 0	cfv	⊢ ( 𝐴 ‘ 𝑦 )
13	11 12	wcel	⊢ ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 )
14	10 13	wi	⊢ ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) )
15	14 7 2	wral	⊢ ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) )
16	15 6 2	wral	⊢ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) )
17	4 5 16	w3a	⊢ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
18	1 17	wb	⊢ ( Smo 𝐴 ↔ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )