![]() |
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. 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 6002 | . 2 ⊢ E Fr On | |
2 | eloni 5973 | . . . 4 ⊢ (𝑥 ∈ On → Ord 𝑥) | |
3 | eloni 5973 | . . . 4 ⊢ (𝑦 ∈ On → Ord 𝑦) | |
4 | ordtri3or 5995 | . . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) | |
5 | epel 5258 | . . . . . 6 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) | |
6 | biid 253 | . . . . . 6 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) | |
7 | epel 5258 | . . . . . 6 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥) | |
8 | 5, 6, 7 | 3orbi123i 1199 | . . . . 5 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
9 | 4, 8 | sylibr 226 | . . . 4 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
10 | 2, 3, 9 | syl2an 589 | . . 3 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
11 | 10 | rgen2a 3186 | . 2 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) |
12 | dfwe2 7242 | . 2 ⊢ ( E We On ↔ ( E Fr On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))) | |
13 | 1, 11, 12 | mpbir2an 702 | 1 ⊢ E We On |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 386 ∨ w3o 1110 ∈ wcel 2164 ∀wral 3117 class class class wbr 4873 E cep 5254 Fr wfr 5298 We wwe 5300 Ord word 5962 Oncon0 5963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 ax-un 7209 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-pss 3814 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-tp 4402 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-tr 4976 df-eprel 5255 df-po 5263 df-so 5264 df-fr 5301 df-we 5303 df-ord 5966 df-on 5967 |
This theorem is referenced by: ordon 7244 omsinds 7345 onnseq 7707 dfrecs3 7735 tfr1ALT 7762 tfr2ALT 7763 tfr3ALT 7764 ordunifi 8479 ordtypelem8 8699 oismo 8714 cantnfcl 8841 leweon 9147 r0weon 9148 ac10ct 9170 dfac12lem2 9281 cflim2 9400 cofsmo 9406 hsmexlem1 9563 smobeth 9723 gruina 9955 ltsopi 10025 dford5 32141 finminlem 32840 dnwech 38454 aomclem4 38463 |
Copyright terms: Public domain | W3C validator |