Theorem dfon2 35906

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.)

Assertion

Ref	Expression
dfon2	⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}

Distinct variable group:   𝑥,𝑦

Proof of Theorem dfon2

Dummy variables 𝑧 𝑤 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-on 6318	. 2 ⊢ On = {𝑥 ∣ Ord 𝑥}
2		tz7.7 6340	. . . . . . . . 9 ⊢ ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦 ∈ 𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥)))
3		df-pss 3918	. . . . . . . . 9 ⊢ (𝑦 ⊊ 𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥))
4	2, 3	bitr4di 289	. . . . . . . 8 ⊢ ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦 ∈ 𝑥 ↔ 𝑦 ⊊ 𝑥))
5	4	exbiri 810	. . . . . . 7 ⊢ (Ord 𝑥 → (Tr 𝑦 → (𝑦 ⊊ 𝑥 → 𝑦 ∈ 𝑥)))
6	5	com23 86	. . . . . 6 ⊢ (Ord 𝑥 → (𝑦 ⊊ 𝑥 → (Tr 𝑦 → 𝑦 ∈ 𝑥)))
7	6	impd 410	. . . . 5 ⊢ (Ord 𝑥 → ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥))
8	7	alrimiv 1928	. . . 4 ⊢ (Ord 𝑥 → ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥))
9		vex 3441	. . . . . . 7 ⊢ 𝑥 ∈ V
10		dfon2lem3 35899	. . . . . . 7 ⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)))
11	9, 10	ax-mp 5	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))
12	11	simpld 494	. . . . 5 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥)
13	9	dfon2lem7 35903	. . . . . . . 8 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝑥 → ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡)))
14	13	ralrimiv 3124	. . . . . . 7 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡))
15		dfon2lem9 35905	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → E Fr 𝑥)
16		psseq2 4040	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → (𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑧))
17	16	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑧 → ((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) ↔ (𝑢 ⊊ 𝑧 ∧ Tr 𝑢)))
18		elequ2 2128	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑧 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧))
19	17, 18	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → (((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧)))
20	19	albidv 1921	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑢((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧)))
21		psseq1 4039	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑣 → (𝑢 ⊊ 𝑧 ↔ 𝑣 ⊊ 𝑧))
22		treq 5209	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑣 → (Tr 𝑢 ↔ Tr 𝑣))
23	21, 22	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑣 → ((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) ↔ (𝑣 ⊊ 𝑧 ∧ Tr 𝑣)))
24		elequ1 2120	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑣 → (𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧))
25	23, 24	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑣 → (((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧) ↔ ((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧)))
26	25	cbvalvw 2037	. . . . . . . . . . . . 13 ⊢ (∀𝑢((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧) ↔ ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧))
27	20, 26	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧)))
28	27	rspccv 3570	. . . . . . . . . . 11 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → (𝑧 ∈ 𝑥 → ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧)))
29		psseq2 4040	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑤 → (𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑤))
30	29	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑤 → ((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) ↔ (𝑢 ⊊ 𝑤 ∧ Tr 𝑢)))
31		elequ2 2128	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑤 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤))
32	30, 31	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑤 → (((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤)))
33	32	albidv 1921	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑢((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤)))
34		psseq1 4039	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑦 → (𝑢 ⊊ 𝑤 ↔ 𝑦 ⊊ 𝑤))
35		treq 5209	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑦 → (Tr 𝑢 ↔ Tr 𝑦))
36	34, 35	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑦 → ((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) ↔ (𝑦 ⊊ 𝑤 ∧ Tr 𝑦)))
37		elequ1 2120	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
38	36, 37	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑦 → (((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤) ↔ ((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)))
39	38	cbvalvw 2037	. . . . . . . . . . . . 13 ⊢ (∀𝑢((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤) ↔ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤))
40	33, 39	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)))
41	40	rspccv 3570	. . . . . . . . . . 11 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → (𝑤 ∈ 𝑥 → ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)))
42	28, 41	anim12d 609	. . . . . . . . . 10 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧) ∧ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤))))
43		vex 3441	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
44		vex 3441	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
45	43, 44	dfon2lem5 35901	. . . . . . . . . 10 ⊢ ((∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧) ∧ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
46	42, 45	syl6 35	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
47	46	ralrimivv 3174	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
48	15, 47	jca 511	. . . . . . 7 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
49	14, 48	syl 17	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
50		dfwe2 7716	. . . . . . 7 ⊢ ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧)))
51		epel 5524	. . . . . . . . . 10 ⊢ (𝑧 E 𝑤 ↔ 𝑧 ∈ 𝑤)
52		biid 261	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 ↔ 𝑧 = 𝑤)
53		epel 5524	. . . . . . . . . 10 ⊢ (𝑤 E 𝑧 ↔ 𝑤 ∈ 𝑧)
54	51, 52, 53	3orbi123i 1156	. . . . . . . . 9 ⊢ ((𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧) ↔ (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
55	54	2ralbii 3108	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧) ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
56	55	anbi2i 623	. . . . . . 7 ⊢ (( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧)) ↔ ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
57	50, 56	bitri 275	. . . . . 6 ⊢ ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
58	49, 57	sylibr 234	. . . . 5 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E We 𝑥)
59		df-ord 6317	. . . . 5 ⊢ (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
60	12, 58, 59	sylanbrc 583	. . . 4 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Ord 𝑥)
61	8, 60	impbii 209	. . 3 ⊢ (Ord 𝑥 ↔ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥))
62	61	abbii 2800	. 2 ⊢ {𝑥 ∣ Ord 𝑥} = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}
63	1, 62	eqtri 2756	1 ⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wal 1539   = wceq 1541   ∈ wcel 2113  {cab 2711   ≠ wne 2929  ∀wral 3048  Vcvv 3437   ⊆ wss 3898   ⊊ wpss 3899   class class class wbr 5095  Tr wtr 5202   E cep 5520   Fr wfr 5571   We wwe 5573  Ord word 6313  Oncon0 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-iin 4946  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318  df-suc 6320

This theorem is referenced by:  dfon3  36006