Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > epweon | Structured version Visualization version GIF version |
Description: The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of [Mendelson] p. 244. (Contributed by NM, 1-Nov-2003.) |
Ref | Expression |
---|---|
epweon | ⊢ E We On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onfr 6211 | . 2 ⊢ E Fr On | |
2 | eloni 6182 | . . . 4 ⊢ (𝑥 ∈ On → Ord 𝑥) | |
3 | eloni 6182 | . . . 4 ⊢ (𝑦 ∈ On → Ord 𝑦) | |
4 | ordtri3or 6204 | . . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) | |
5 | epel 5437 | . . . . . 6 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) | |
6 | biid 264 | . . . . . 6 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) | |
7 | epel 5437 | . . . . . 6 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥) | |
8 | 5, 6, 7 | 3orbi123i 1157 | . . . . 5 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
9 | 4, 8 | sylibr 237 | . . . 4 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
10 | 2, 3, 9 | syl2an 599 | . . 3 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
11 | 10 | rgen2 3115 | . 2 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) |
12 | dfwe2 7515 | . 2 ⊢ ( E We On ↔ ( E Fr On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))) | |
13 | 1, 11, 12 | mpbir2an 711 | 1 ⊢ E We On |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 ∨ w3o 1087 ∈ wcel 2114 ∀wral 3053 class class class wbr 5030 E cep 5433 Fr wfr 5480 We wwe 5482 Ord word 6171 Oncon0 6172 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-11 2162 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 ax-un 7479 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-tr 5137 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-ord 6175 df-on 6176 |
This theorem is referenced by: ordon 7517 omsinds 7619 onnseq 8010 dfrecs3 8038 tfr1ALT 8065 tfr2ALT 8066 tfr3ALT 8067 ordunifi 8842 ordtypelem8 9062 oismo 9077 cantnfcl 9203 leweon 9511 r0weon 9512 ac10ct 9534 dfac12lem2 9644 cflim2 9763 cofsmo 9769 hsmexlem1 9926 smobeth 10086 gruina 10318 ltsopi 10388 dford5 33244 on2recsfn 33467 on2recsov 33468 on2ind 33469 on3ind 33470 finminlem 34145 dnwech 40445 aomclem4 40454 |
Copyright terms: Public domain | W3C validator |