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 \leftrightarrow (A : dom A ⟶ On \land Ord dom A \land \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in 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 \in y$
11	8 0	cfv	$class A (x)$
12	9 0	cfv	$class A (y)$
13	11 12	wcel	$wff A (x) \in A (y)$
14	10 13	wi	$wff (x \in y \to A (x) \in A (y))$
15	14 7 2	wral	$wff \forall y \in dom A (x \in y \to A (x) \in A (y))$
16	15 6 2	wral	$wff \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y))$
17	4 5 16	w3a	$wff (A : dom A ⟶ On \land Ord dom A \land \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)))$
18	1 17	wb	$wff (Smo A \leftrightarrow (A : dom A ⟶ On \land Ord dom A \land \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y))))$