Theorem 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 = { 𝑥 ∣ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) }

Proof

Step	Hyp	Ref	Expression
1		df-on	⊢ On = { 𝑥 ∣ Ord 𝑥 }
2		tz7.7	⊢ ( ( Ord 𝑥 ∧ Tr 𝑦 ) → ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥 ) ) )
3		df-pss	⊢ ( 𝑦 ⊊ 𝑥 ↔ ( 𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥 ) )
4	2 3	bitr4di	⊢ ( ( Ord 𝑥 ∧ Tr 𝑦 ) → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ⊊ 𝑥 ) )
5	4	exbiri	⊢ ( Ord 𝑥 → ( Tr 𝑦 → ( 𝑦 ⊊ 𝑥 → 𝑦 ∈ 𝑥 ) ) )
6	5	com23	⊢ ( Ord 𝑥 → ( 𝑦 ⊊ 𝑥 → ( Tr 𝑦 → 𝑦 ∈ 𝑥 ) ) )
7	6	impd	⊢ ( Ord 𝑥 → ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) )
8	7	alrimiv	⊢ ( Ord 𝑥 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) )
9		vex	⊢ 𝑥 ∈ V
10		dfon2lem3	⊢ ( 𝑥 ∈ V → ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ( Tr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 ) ) )
11	9 10	ax-mp	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ( Tr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 ) )
12	11	simpld	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → Tr 𝑥 )
13	9	dfon2lem7	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ( 𝑡 ∈ 𝑥 → ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) ) )
14	13	ralrimiv	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) )
15		dfon2lem9	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) → E Fr 𝑥 )
16		psseq2	⊢ ( 𝑡 = 𝑧 → ( 𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑧 ) )
17	16	anbi1d	⊢ ( 𝑡 = 𝑧 → ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) ↔ ( 𝑢 ⊊ 𝑧 ∧ Tr 𝑢 ) ) )
18		elequ2	⊢ ( 𝑡 = 𝑧 → ( 𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧 ) )
19	17 18	imbi12d	⊢ ( 𝑡 = 𝑧 → ( ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) ↔ ( ( 𝑢 ⊊ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑧 ) ) )
20	19	albidv	⊢ ( 𝑡 = 𝑧 → ( ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) ↔ ∀ 𝑢 ( ( 𝑢 ⊊ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑧 ) ) )
21		psseq1	⊢ ( 𝑢 = 𝑣 → ( 𝑢 ⊊ 𝑧 ↔ 𝑣 ⊊ 𝑧 ) )
22		treq	⊢ ( 𝑢 = 𝑣 → ( Tr 𝑢 ↔ Tr 𝑣 ) )
23	21 22	anbi12d	⊢ ( 𝑢 = 𝑣 → ( ( 𝑢 ⊊ 𝑧 ∧ Tr 𝑢 ) ↔ ( 𝑣 ⊊ 𝑧 ∧ Tr 𝑣 ) ) )
24		elequ1	⊢ ( 𝑢 = 𝑣 → ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) )
25	23 24	imbi12d	⊢ ( 𝑢 = 𝑣 → ( ( ( 𝑢 ⊊ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑧 ) ↔ ( ( 𝑣 ⊊ 𝑧 ∧ Tr 𝑣 ) → 𝑣 ∈ 𝑧 ) ) )
26	25	cbvalvw	⊢ ( ∀ 𝑢 ( ( 𝑢 ⊊ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑧 ) ↔ ∀ 𝑣 ( ( 𝑣 ⊊ 𝑧 ∧ Tr 𝑣 ) → 𝑣 ∈ 𝑧 ) )
27	20 26	bitrdi	⊢ ( 𝑡 = 𝑧 → ( ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) ↔ ∀ 𝑣 ( ( 𝑣 ⊊ 𝑧 ∧ Tr 𝑣 ) → 𝑣 ∈ 𝑧 ) ) )
28	27	rspccv	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) → ( 𝑧 ∈ 𝑥 → ∀ 𝑣 ( ( 𝑣 ⊊ 𝑧 ∧ Tr 𝑣 ) → 𝑣 ∈ 𝑧 ) ) )
29		psseq2	⊢ ( 𝑡 = 𝑤 → ( 𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑤 ) )
30	29	anbi1d	⊢ ( 𝑡 = 𝑤 → ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) ↔ ( 𝑢 ⊊ 𝑤 ∧ Tr 𝑢 ) ) )
31		elequ2	⊢ ( 𝑡 = 𝑤 → ( 𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤 ) )
32	30 31	imbi12d	⊢ ( 𝑡 = 𝑤 → ( ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) ↔ ( ( 𝑢 ⊊ 𝑤 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑤 ) ) )
33	32	albidv	⊢ ( 𝑡 = 𝑤 → ( ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) ↔ ∀ 𝑢 ( ( 𝑢 ⊊ 𝑤 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑤 ) ) )
34		psseq1	⊢ ( 𝑢 = 𝑦 → ( 𝑢 ⊊ 𝑤 ↔ 𝑦 ⊊ 𝑤 ) )
35		treq	⊢ ( 𝑢 = 𝑦 → ( Tr 𝑢 ↔ Tr 𝑦 ) )
36	34 35	anbi12d	⊢ ( 𝑢 = 𝑦 → ( ( 𝑢 ⊊ 𝑤 ∧ Tr 𝑢 ) ↔ ( 𝑦 ⊊ 𝑤 ∧ Tr 𝑦 ) ) )
37		elequ1	⊢ ( 𝑢 = 𝑦 → ( 𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤 ) )
38	36 37	imbi12d	⊢ ( 𝑢 = 𝑦 → ( ( ( 𝑢 ⊊ 𝑤 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑤 ) ↔ ( ( 𝑦 ⊊ 𝑤 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑤 ) ) )
39	38	cbvalvw	⊢ ( ∀ 𝑢 ( ( 𝑢 ⊊ 𝑤 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑤 ) ↔ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑤 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑤 ) )
40	33 39	bitrdi	⊢ ( 𝑡 = 𝑤 → ( ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) ↔ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑤 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑤 ) ) )
41	40	rspccv	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) → ( 𝑤 ∈ 𝑥 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑤 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑤 ) ) )
42	28 41	anim12d	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ∀ 𝑣 ( ( 𝑣 ⊊ 𝑧 ∧ Tr 𝑣 ) → 𝑣 ∈ 𝑧 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑤 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑤 ) ) ) )
43		vex	⊢ 𝑧 ∈ V
44		vex	⊢ 𝑤 ∈ V
45	43 44	dfon2lem5	⊢ ( ( ∀ 𝑣 ( ( 𝑣 ⊊ 𝑧 ∧ Tr 𝑣 ) → 𝑣 ∈ 𝑧 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑤 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑤 ) ) → ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) )
46	42 45	syl6	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
47	46	ralrimivv	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) → ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) )
48	15 47	jca	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑢 ( ( 𝑢 ⊊ 𝑡 ∧ Tr 𝑢 ) → 𝑢 ∈ 𝑡 ) → ( E Fr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
49	14 48	syl	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ( E Fr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
50		dfwe2	⊢ ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧 ) ) )
51		epel	⊢ ( 𝑧 E 𝑤 ↔ 𝑧 ∈ 𝑤 )
52		biid	⊢ ( 𝑧 = 𝑤 ↔ 𝑧 = 𝑤 )
53		epel	⊢ ( 𝑤 E 𝑧 ↔ 𝑤 ∈ 𝑧 )
54	51 52 53	3orbi123i	⊢ ( ( 𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧 ) ↔ ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) )
55	54	2ralbii	⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) )
56	55	anbi2i	⊢ ( ( E Fr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧 ) ) ↔ ( E Fr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
57	50 56	bitri	⊢ ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
58	49 57	sylibr	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → E We 𝑥 )
59		df-ord	⊢ ( Ord 𝑥 ↔ ( Tr 𝑥 ∧ E We 𝑥 ) )
60	12 58 59	sylanbrc	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → Ord 𝑥 )
61	8 60	impbii	⊢ ( Ord 𝑥 ↔ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) )
62	61	abbii	⊢ { 𝑥 ∣ Ord 𝑥 } = { 𝑥 ∣ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) }
63	1 62	eqtri	⊢ On = { 𝑥 ∣ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) }