MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-smo Structured version   Visualization version   GIF version

Definition df-smo 7303
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
StepHypRef Expression
1 cA . . 3 class 𝐴
21wsmo 7302 . 2 wff Smo 𝐴
31cdm 5024 . . . 4 class dom 𝐴
4 con0 5622 . . . 4 class On
53, 4, 1wf 5782 . . 3 wff 𝐴:dom 𝐴⟶On
63word 5621 . . 3 wff Ord dom 𝐴
7 vx . . . . . . 7 setvar 𝑥
8 vy . . . . . . 7 setvar 𝑦
97, 8wel 1976 . . . . . 6 wff 𝑥𝑦
107cv 1473 . . . . . . . 8 class 𝑥
1110, 1cfv 5786 . . . . . . 7 class (𝐴𝑥)
128cv 1473 . . . . . . . 8 class 𝑦
1312, 1cfv 5786 . . . . . . 7 class (𝐴𝑦)
1411, 13wcel 1975 . . . . . 6 wff (𝐴𝑥) ∈ (𝐴𝑦)
159, 14wi 4 . . . . 5 wff (𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))
1615, 8, 3wral 2891 . . . 4 wff 𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))
1716, 7, 3wral 2891 . . 3 wff 𝑥 ∈ dom 𝐴𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))
185, 6, 17w3a 1030 . 2 wff (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦)))
192, 18wb 194 1 wff (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  dfsmo2  7304  issmo  7305  smoeq  7307  smodm  7308  smores  7309  smofvon  7316  smoel  7317  smoiso  7319
  Copyright terms: Public domain W3C validator