Theorem dfon2 35815

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 6361	. 2 ⊢ On = {𝑥 ∣ Ord 𝑥}
2		tz7.7 6383	. . . . . . . . 9 ⊢ ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦 ∈ 𝑥 ↔ (𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥)))
3		df-pss 3951	. . . . . . . . 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 1927	. . . 4 ⊢ (Ord 𝑥 → ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥))
9		vex 3468	. . . . . . 7 ⊢ 𝑥 ∈ V
10		dfon2lem3 35808	. . . . . . 7 ⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)))
11	9, 10	ax-mp 5	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))
12	11	simpld 494	. . . . 5 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥)
13	9	dfon2lem7 35812	. . . . . . . 8 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝑥 → ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡)))
14	13	ralrimiv 3132	. . . . . . 7 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡))
15		dfon2lem9 35814	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → E Fr 𝑥)
16		psseq2 4071	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → (𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑧))
17	16	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑧 → ((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) ↔ (𝑢 ⊊ 𝑧 ∧ Tr 𝑢)))
18		elequ2 2124	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑧 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧))
19	17, 18	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → (((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧)))
20	19	albidv 1920	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑢((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧)))
21		psseq1 4070	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑣 → (𝑢 ⊊ 𝑧 ↔ 𝑣 ⊊ 𝑧))
22		treq 5242	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑣 → (Tr 𝑢 ↔ Tr 𝑣))
23	21, 22	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑣 → ((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) ↔ (𝑣 ⊊ 𝑧 ∧ Tr 𝑣)))
24		elequ1 2116	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑣 → (𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧))
25	23, 24	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑣 → (((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧) ↔ ((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧)))
26	25	cbvalvw 2036	. . . . . . . . . . . . 13 ⊢ (∀𝑢((𝑢 ⊊ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ 𝑧) ↔ ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧))
27	20, 26	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧)))
28	27	rspccv 3603	. . . . . . . . . . 11 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → (𝑧 ∈ 𝑥 → ∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧)))
29		psseq2 4071	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑤 → (𝑢 ⊊ 𝑡 ↔ 𝑢 ⊊ 𝑤))
30	29	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑤 → ((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) ↔ (𝑢 ⊊ 𝑤 ∧ Tr 𝑢)))
31		elequ2 2124	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑤 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤))
32	30, 31	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑤 → (((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤)))
33	32	albidv 1920	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑢((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤)))
34		psseq1 4070	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑦 → (𝑢 ⊊ 𝑤 ↔ 𝑦 ⊊ 𝑤))
35		treq 5242	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑦 → (Tr 𝑢 ↔ Tr 𝑦))
36	34, 35	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑦 → ((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) ↔ (𝑦 ⊊ 𝑤 ∧ Tr 𝑦)))
37		elequ1 2116	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
38	36, 37	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑦 → (((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤) ↔ ((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)))
39	38	cbvalvw 2036	. . . . . . . . . . . . 13 ⊢ (∀𝑢((𝑢 ⊊ 𝑤 ∧ Tr 𝑢) → 𝑢 ∈ 𝑤) ↔ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤))
40	33, 39	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → (∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) ↔ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)))
41	40	rspccv 3603	. . . . . . . . . . 11 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → (𝑤 ∈ 𝑥 → ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)))
42	28, 41	anim12d 609	. . . . . . . . . 10 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧) ∧ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤))))
43		vex 3468	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
44		vex 3468	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
45	43, 44	dfon2lem5 35810	. . . . . . . . . 10 ⊢ ((∀𝑣((𝑣 ⊊ 𝑧 ∧ Tr 𝑣) → 𝑣 ∈ 𝑧) ∧ ∀𝑦((𝑦 ⊊ 𝑤 ∧ Tr 𝑦) → 𝑦 ∈ 𝑤)) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
46	42, 45	syl6 35	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
47	46	ralrimivv 3186	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
48	15, 47	jca 511	. . . . . . 7 ⊢ (∀𝑡 ∈ 𝑥 ∀𝑢((𝑢 ⊊ 𝑡 ∧ Tr 𝑢) → 𝑢 ∈ 𝑡) → ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
49	14, 48	syl 17	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)))
50		dfwe2 7773	. . . . . . 7 ⊢ ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧)))
51		epel 5561	. . . . . . . . . 10 ⊢ (𝑧 E 𝑤 ↔ 𝑧 ∈ 𝑤)
52		biid 261	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 ↔ 𝑧 = 𝑤)
53		epel 5561	. . . . . . . . . 10 ⊢ (𝑤 E 𝑧 ↔ 𝑤 ∈ 𝑧)
54	51, 52, 53	3orbi123i 1156	. . . . . . . . 9 ⊢ ((𝑧 E 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 E 𝑧) ↔ (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
55	54	2ralbii 3116	. . . . . . . 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 6360	. . . . 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 2803	. 2 ⊢ {𝑥 ∣ Ord 𝑥} = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}
63	1, 62	eqtri 2759	1 ⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2714   ≠ wne 2933  ∀wral 3052  Vcvv 3464   ⊆ wss 3931   ⊊ wpss 3932   class class class wbr 5124  Tr wtr 5234   E cep 5557   Fr wfr 5608   We wwe 5610  Ord word 6356  Oncon0 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-iin 4975  df-br 5125  df-opab 5187  df-tr 5235  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361  df-suc 6363

This theorem is referenced by:  dfon3  35915