dfon2

Description: On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011)

		Ref	Expression
	Assertion	dfon2	$⊢ On = \{x \| \forall y ((y \subset x \land Tr y) \to y \in x)\}$

Proof

Step	Hyp	Ref	Expression
1		df-on	$⊢ On = \{x \| Ord x\}$
2		tz7.7	$⊢ (Ord x \land Tr y) \to (y \in x \leftrightarrow (y \subseteq x \land y \neq x))$
3		df-pss	$⊢ y \subset x \leftrightarrow (y \subseteq x \land y \neq x)$
4	2 3	bitr4di	$⊢ (Ord x \land Tr y) \to (y \in x \leftrightarrow y \subset x)$
5	4	exbiri	$⊢ Ord x \to (Tr y \to (y \subset x \to y \in x))$
6	5	com23	$⊢ Ord x \to (y \subset x \to (Tr y \to y \in x))$
7	6	impd	$⊢ Ord x \to ((y \subset x \land Tr y) \to y \in x)$
8	7	alrimiv	$⊢ Ord x \to \forall y ((y \subset x \land Tr y) \to y \in x)$
9		vex	$⊢ x \in V$
10		dfon2lem3	$⊢ x \in V \to (\forall y ((y \subset x \land Tr y) \to y \in x) \to (Tr x \land \forall z \in x \neg z \in z))$
11	9 10	ax-mp	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to (Tr x \land \forall z \in x \neg z \in z)$
12	11	simpld	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to Tr x$
13	9	dfon2lem7	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to (t \in x \to \forall u ((u \subset t \land Tr u) \to u \in t))$
14	13	ralrimiv	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t)$
15		dfon2lem9	$⊢ \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t) \to E Fr x$
16		psseq2	$⊢ t = z \to (u \subset t \leftrightarrow u \subset z)$
17	16	anbi1d	$⊢ t = z \to ((u \subset t \land Tr u) \leftrightarrow (u \subset z \land Tr u))$
18		elequ2	$⊢ t = z \to (u \in t \leftrightarrow u \in z)$
19	17 18	imbi12d	$⊢ t = z \to (((u \subset t \land Tr u) \to u \in t) \leftrightarrow ((u \subset z \land Tr u) \to u \in z))$
20	19	albidv	$⊢ t = z \to (\forall u ((u \subset t \land Tr u) \to u \in t) \leftrightarrow \forall u ((u \subset z \land Tr u) \to u \in z))$
21		psseq1	$⊢ u = v \to (u \subset z \leftrightarrow v \subset z)$
22		treq	$⊢ u = v \to (Tr u \leftrightarrow Tr v)$
23	21 22	anbi12d	$⊢ u = v \to ((u \subset z \land Tr u) \leftrightarrow (v \subset z \land Tr v))$
24		elequ1	$⊢ u = v \to (u \in z \leftrightarrow v \in z)$
25	23 24	imbi12d	$⊢ u = v \to (((u \subset z \land Tr u) \to u \in z) \leftrightarrow ((v \subset z \land Tr v) \to v \in z))$
26	25	cbvalvw	$⊢ \forall u ((u \subset z \land Tr u) \to u \in z) \leftrightarrow \forall v ((v \subset z \land Tr v) \to v \in z)$
27	20 26	bitrdi	$⊢ t = z \to (\forall u ((u \subset t \land Tr u) \to u \in t) \leftrightarrow \forall v ((v \subset z \land Tr v) \to v \in z))$
28	27	rspccv	$⊢ \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t) \to (z \in x \to \forall v ((v \subset z \land Tr v) \to v \in z))$
29		psseq2	$⊢ t = w \to (u \subset t \leftrightarrow u \subset w)$
30	29	anbi1d	$⊢ t = w \to ((u \subset t \land Tr u) \leftrightarrow (u \subset w \land Tr u))$
31		elequ2	$⊢ t = w \to (u \in t \leftrightarrow u \in w)$
32	30 31	imbi12d	$⊢ t = w \to (((u \subset t \land Tr u) \to u \in t) \leftrightarrow ((u \subset w \land Tr u) \to u \in w))$
33	32	albidv	$⊢ t = w \to (\forall u ((u \subset t \land Tr u) \to u \in t) \leftrightarrow \forall u ((u \subset w \land Tr u) \to u \in w))$
34		psseq1	$⊢ u = y \to (u \subset w \leftrightarrow y \subset w)$
35		treq	$⊢ u = y \to (Tr u \leftrightarrow Tr y)$
36	34 35	anbi12d	$⊢ u = y \to ((u \subset w \land Tr u) \leftrightarrow (y \subset w \land Tr y))$
37		elequ1	$⊢ u = y \to (u \in w \leftrightarrow y \in w)$
38	36 37	imbi12d	$⊢ u = y \to (((u \subset w \land Tr u) \to u \in w) \leftrightarrow ((y \subset w \land Tr y) \to y \in w))$
39	38	cbvalvw	$⊢ \forall u ((u \subset w \land Tr u) \to u \in w) \leftrightarrow \forall y ((y \subset w \land Tr y) \to y \in w)$
40	33 39	bitrdi	$⊢ t = w \to (\forall u ((u \subset t \land Tr u) \to u \in t) \leftrightarrow \forall y ((y \subset w \land Tr y) \to y \in w))$
41	40	rspccv	$⊢ \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t) \to (w \in x \to \forall y ((y \subset w \land Tr y) \to y \in w))$
42	28 41	anim12d	$⊢ \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t) \to ((z \in x \land w \in x) \to (\forall v ((v \subset z \land Tr v) \to v \in z) \land \forall y ((y \subset w \land Tr y) \to y \in w)))$
43		vex	$⊢ z \in V$
44		vex	$⊢ w \in V$
45	43 44	dfon2lem5	$⊢ (\forall v ((v \subset z \land Tr v) \to v \in z) \land \forall y ((y \subset w \land Tr y) \to y \in w)) \to (z \in w \lor z = w \lor w \in z)$
46	42 45	syl6	$⊢ \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t) \to ((z \in x \land w \in x) \to (z \in w \lor z = w \lor w \in z))$
47	46	ralrimivv	$⊢ \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t) \to \forall z \in x \forall w \in x (z \in w \lor z = w \lor w \in z)$
48	15 47	jca	$⊢ \forall t \in x \forall u ((u \subset t \land Tr u) \to u \in t) \to (E Fr x \land \forall z \in x \forall w \in x (z \in w \lor z = w \lor w \in z))$
49	14 48	syl	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to (E Fr x \land \forall z \in x \forall w \in x (z \in w \lor z = w \lor w \in z))$
50		dfwe2	$⊢ E We x \leftrightarrow (E Fr x \land \forall z \in x \forall w \in x (z E w \lor z = w \lor w E z))$
51		epel	$⊢ z E w \leftrightarrow z \in w$
52		biid	$⊢ z = w \leftrightarrow z = w$
53		epel	$⊢ w E z \leftrightarrow w \in z$
54	51 52 53	3orbi123i	$⊢ (z E w \lor z = w \lor w E z) \leftrightarrow (z \in w \lor z = w \lor w \in z)$
55	54	2ralbii	$⊢ \forall z \in x \forall w \in x (z E w \lor z = w \lor w E z) \leftrightarrow \forall z \in x \forall w \in x (z \in w \lor z = w \lor w \in z)$
56	55	anbi2i	$⊢ (E Fr x \land \forall z \in x \forall w \in x (z E w \lor z = w \lor w E z)) \leftrightarrow (E Fr x \land \forall z \in x \forall w \in x (z \in w \lor z = w \lor w \in z))$
57	50 56	bitri	$⊢ E We x \leftrightarrow (E Fr x \land \forall z \in x \forall w \in x (z \in w \lor z = w \lor w \in z))$
58	49 57	sylibr	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to E We x$
59		df-ord	$⊢ Ord x \leftrightarrow (Tr x \land E We x)$
60	12 58 59	sylanbrc	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to Ord x$
61	8 60	impbii	$⊢ Ord x \leftrightarrow \forall y ((y \subset x \land Tr y) \to y \in x)$
62	61	abbii	$⊢ \{x \| Ord x\} = \{x \| \forall y ((y \subset x \land Tr y) \to y \in x)\}$
63	1 62	eqtri	$⊢ On = \{x \| \forall y ((y \subset x \land Tr y) \to y \in x)\}$

Metamath Proof Explorer

Theorem dfon2

Proof