dfsmo2

Description: Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013)

		Ref	Expression
	Assertion	dfsmo2	$⊢ Smo F \leftrightarrow (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x))$

Proof

Step	Hyp	Ref	Expression
1		df-smo	$⊢ Smo F \leftrightarrow (F : dom F ⟶ On \land Ord dom F \land \forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x)))$
2		ralcom	$⊢ \forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x)) \leftrightarrow \forall x \in dom F \forall y \in dom F (y \in x \to F (y) \in F (x))$
3		impexp	$⊢ ((y \in dom F \land y \in x) \to F (y) \in F (x)) \leftrightarrow (y \in dom F \to (y \in x \to F (y) \in F (x)))$
4		simpr	$⊢ (y \in dom F \land y \in x) \to y \in x$
5		ordtr1	$⊢ Ord dom F \to ((y \in x \land x \in dom F) \to y \in dom F)$
6	5	3impib	$⊢ (Ord dom F \land y \in x \land x \in dom F) \to y \in dom F$
7	6	3com23	$⊢ (Ord dom F \land x \in dom F \land y \in x) \to y \in dom F$
8		simp3	$⊢ (Ord dom F \land x \in dom F \land y \in x) \to y \in x$
9	7 8	jca	$⊢ (Ord dom F \land x \in dom F \land y \in x) \to (y \in dom F \land y \in x)$
10	9	3expia	$⊢ (Ord dom F \land x \in dom F) \to (y \in x \to (y \in dom F \land y \in x))$
11	4 10	impbid2	$⊢ (Ord dom F \land x \in dom F) \to ((y \in dom F \land y \in x) \leftrightarrow y \in x)$
12	11	imbi1d	$⊢ (Ord dom F \land x \in dom F) \to (((y \in dom F \land y \in x) \to F (y) \in F (x)) \leftrightarrow (y \in x \to F (y) \in F (x)))$
13	3 12	bitr3id	$⊢ (Ord dom F \land x \in dom F) \to ((y \in dom F \to (y \in x \to F (y) \in F (x))) \leftrightarrow (y \in x \to F (y) \in F (x)))$
14	13	ralbidv2	$⊢ (Ord dom F \land x \in dom F) \to (\forall y \in dom F (y \in x \to F (y) \in F (x)) \leftrightarrow \forall y \in x F (y) \in F (x))$
15	14	ralbidva	$⊢ Ord dom F \to (\forall x \in dom F \forall y \in dom F (y \in x \to F (y) \in F (x)) \leftrightarrow \forall x \in dom F \forall y \in x F (y) \in F (x))$
16	2 15	bitrid	$⊢ Ord dom F \to (\forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x)) \leftrightarrow \forall x \in dom F \forall y \in x F (y) \in F (x))$
17	16	pm5.32i	$⊢ (Ord dom F \land \forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x))) \leftrightarrow (Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x))$
18	17	anbi2i	$⊢ (F : dom F ⟶ On \land (Ord dom F \land \forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x)))) \leftrightarrow (F : dom F ⟶ On \land (Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x)))$
19		3anass	$⊢ (F : dom F ⟶ On \land Ord dom F \land \forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x))) \leftrightarrow (F : dom F ⟶ On \land (Ord dom F \land \forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x))))$
20		3anass	$⊢ (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x)) \leftrightarrow (F : dom F ⟶ On \land (Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x)))$
21	18 19 20	3bitr4i	$⊢ (F : dom F ⟶ On \land Ord dom F \land \forall y \in dom F \forall x \in dom F (y \in x \to F (y) \in F (x))) \leftrightarrow (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x))$
22	1 21	bitri	$⊢ Smo F \leftrightarrow (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x))$

Metamath Proof Explorer

Theorem dfsmo2

Proof