![]() |
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. For a shorter proof requiring ax-un 7729, see epweonALT 7767. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7729. (Revised by BTernaryTau, 30-Nov-2024.) |
Ref | Expression |
---|---|
epweon | ⊢ E We On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onfr 6404 | . 2 ⊢ E Fr On | |
2 | df-po 5589 | . . . 4 ⊢ ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) | |
3 | eloni 6375 | . . . . . . . . 9 ⊢ (𝑥 ∈ On → Ord 𝑥) | |
4 | ordirr 6383 | . . . . . . . . 9 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥) | |
5 | 3, 4 | syl 17 | . . . . . . . 8 ⊢ (𝑥 ∈ On → ¬ 𝑥 ∈ 𝑥) |
6 | epel 5584 | . . . . . . . 8 ⊢ (𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥) | |
7 | 5, 6 | sylnibr 328 | . . . . . . 7 ⊢ (𝑥 ∈ On → ¬ 𝑥 E 𝑥) |
8 | ontr1 6411 | . . . . . . . 8 ⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) | |
9 | epel 5584 | . . . . . . . . 9 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) | |
10 | epel 5584 | . . . . . . . . 9 ⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧) | |
11 | 9, 10 | anbi12i 625 | . . . . . . . 8 ⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧)) |
12 | epel 5584 | . . . . . . . 8 ⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧) | |
13 | 8, 11, 12 | 3imtr4g 295 | . . . . . . 7 ⊢ (𝑧 ∈ On → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)) |
14 | 7, 13 | anim12i 611 | . . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) |
15 | 14 | ralrimiva 3144 | . . . . 5 ⊢ (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) |
16 | 15 | ralrimivw 3148 | . . . 4 ⊢ (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) |
17 | 2, 16 | mprgbir 3066 | . . 3 ⊢ E Po On |
18 | eloni 6375 | . . . . 5 ⊢ (𝑦 ∈ On → Ord 𝑦) | |
19 | ordtri3or 6397 | . . . . . 6 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) | |
20 | biid 260 | . . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) | |
21 | epel 5584 | . . . . . . 7 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥) | |
22 | 9, 20, 21 | 3orbi123i 1154 | . . . . . 6 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
23 | 19, 22 | sylibr 233 | . . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
24 | 3, 18, 23 | syl2an 594 | . . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
25 | 24 | rgen2 3195 | . . 3 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) |
26 | df-so 5590 | . . 3 ⊢ ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))) | |
27 | 17, 25, 26 | mpbir2an 707 | . 2 ⊢ E Or On |
28 | df-we 5634 | . 2 ⊢ ( E We On ↔ ( E Fr On ∧ E Or On)) | |
29 | 1, 27, 28 | mpbir2an 707 | 1 ⊢ E We On |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 ∨ w3o 1084 ∈ wcel 2104 ∀wral 3059 class class class wbr 5149 E cep 5580 Po wpo 5587 Or wor 5588 Fr wfr 5629 We wwe 5631 Ord word 6364 Oncon0 6365 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-ord 6368 df-on 6369 |
This theorem is referenced by: ordon 7768 dford5 7775 omsinds 7880 omsindsOLD 7881 onnseq 8348 dfrecs3 8376 dfrecs3OLD 8377 tfr1ALT 8404 tfr2ALT 8405 tfr3ALT 8406 on2recsfn 8670 on2recsov 8671 on2ind 8672 on3ind 8673 ordunifi 9297 ordtypelem8 9524 oismo 9539 cantnfcl 9666 leweon 10010 r0weon 10011 ac10ct 10033 dfac12lem2 10143 cflim2 10262 cofsmo 10268 hsmexlem1 10425 smobeth 10585 gruina 10817 ltsopi 10887 finminlem 35508 dnwech 42094 aomclem4 42103 onsupuni 42282 oninfint 42289 epsoon 42306 epirron 42307 oneptr 42308 oaun3lem1 42428 |
Copyright terms: Public domain | W3C validator |