Metamath Proof Explorer

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 ⁡ A ↔ A : dom ⁡ A ⟶ On ∧ Ord ⁡ dom ⁡ A ∧ ∀ x ∈ dom ⁡ A ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 wsmo wff Smo ⁡ A
2 0 cdm class dom ⁡ A
3 con0 class On
4 2 3 0 wf wff A : dom ⁡ A ⟶ On
5 2 word wff Ord ⁡ dom ⁡ A
6 vx setvar x
7 vy setvar y
8 6 cv setvar x
9 7 cv setvar y
10 8 9 wcel wff x ∈ y
11 8 0 cfv class A ⁡ x
12 9 0 cfv class A ⁡ y
13 11 12 wcel wff A ⁡ x ∈ A ⁡ y
14 10 13 wi wff x ∈ y → A ⁡ x ∈ A ⁡ y
15 14 7 2 wral wff ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y
16 15 6 2 wral wff ∀ x ∈ dom ⁡ A ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y
17 4 5 16 w3a wff A : dom ⁡ A ⟶ On ∧ Ord ⁡ dom ⁡ A ∧ ∀ x ∈ dom ⁡ A ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y
18 1 17 wb wff Smo ⁡ A ↔ A : dom ⁡ A ⟶ On ∧ Ord ⁡ dom ⁡ A ∧ ∀ x ∈ dom ⁡ A ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y