Definition df-smo 8365

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

Assertion

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

Distinct variable group:   𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-smo

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wsmo 8364	. 2 wff Smo 𝐴
3	1	cdm 5659	. . . 4 class dom 𝐴
4		con0 6357	. . . 4 class On
5	3, 4, 1	wf 6532	. . 3 wff 𝐴:dom 𝐴⟶On
6	3	word 6356	. . 3 wff Ord dom 𝐴
7		vx	. . . . . . 7 setvar 𝑥
8		vy	. . . . . . 7 setvar 𝑦
9	7, 8	wel 2110	. . . . . 6 wff 𝑥 ∈ 𝑦
10	7	cv 1539	. . . . . . . 8 class 𝑥
11	10, 1	cfv 6536	. . . . . . 7 class (𝐴‘𝑥)
12	8	cv 1539	. . . . . . . 8 class 𝑦
13	12, 1	cfv 6536	. . . . . . 7 class (𝐴‘𝑦)
14	11, 13	wcel 2109	. . . . . 6 wff (𝐴‘𝑥) ∈ (𝐴‘𝑦)
15	9, 14	wi 4	. . . . 5 wff (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))
16	15, 8, 3	wral 3052	. . . 4 wff ∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))
17	16, 7, 3	wral 3052	. . 3 wff ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))
18	5, 6, 17	w3a 1086	. 2 wff (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))
19	2, 18	wb 206	1 wff (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))))

This definition is referenced by:  dfsmo2  8366  issmo  8367  smoeq  8369  smodm  8370  smores  8371  smofvon  8378  smoel  8379  smoiso  8381