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.) Avoid ax-un 7588. (Revised by BTernaryTau, 30-Nov-2024.) |
Ref | Expression |
---|---|
epweon | ⊢ E We On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onfr 6305 | . 2 ⊢ E Fr On | |
2 | df-po 5503 | . . . 4 ⊢ ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) | |
3 | eloni 6276 | . . . . . . . . 9 ⊢ (𝑥 ∈ On → Ord 𝑥) | |
4 | ordirr 6284 | . . . . . . . . 9 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥) | |
5 | 3, 4 | syl 17 | . . . . . . . 8 ⊢ (𝑥 ∈ On → ¬ 𝑥 ∈ 𝑥) |
6 | epel 5498 | . . . . . . . 8 ⊢ (𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥) | |
7 | 5, 6 | sylnibr 329 | . . . . . . 7 ⊢ (𝑥 ∈ On → ¬ 𝑥 E 𝑥) |
8 | ontr1 6312 | . . . . . . . 8 ⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) | |
9 | epel 5498 | . . . . . . . . 9 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) | |
10 | epel 5498 | . . . . . . . . 9 ⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧) | |
11 | 9, 10 | anbi12i 627 | . . . . . . . 8 ⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧)) |
12 | epel 5498 | . . . . . . . 8 ⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧) | |
13 | 8, 11, 12 | 3imtr4g 296 | . . . . . . 7 ⊢ (𝑧 ∈ On → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)) |
14 | 7, 13 | anim12i 613 | . . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) |
15 | 14 | ralrimiva 3103 | . . . . 5 ⊢ (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) |
16 | 15 | ralrimivw 3104 | . . . 4 ⊢ (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) |
17 | 2, 16 | mprgbir 3079 | . . 3 ⊢ E Po On |
18 | eloni 6276 | . . . . 5 ⊢ (𝑦 ∈ On → Ord 𝑦) | |
19 | ordtri3or 6298 | . . . . . 6 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) | |
20 | biid 260 | . . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) | |
21 | epel 5498 | . . . . . . 7 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥) | |
22 | 9, 20, 21 | 3orbi123i 1155 | . . . . . 6 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
23 | 19, 22 | sylibr 233 | . . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
24 | 3, 18, 23 | syl2an 596 | . . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
25 | 24 | rgen2 3120 | . . 3 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) |
26 | df-so 5504 | . . 3 ⊢ ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))) | |
27 | 17, 25, 26 | mpbir2an 708 | . 2 ⊢ E Or On |
28 | df-we 5546 | . 2 ⊢ ( E We On ↔ ( E Fr On ∧ E Or On)) | |
29 | 1, 27, 28 | mpbir2an 708 | 1 ⊢ E We On |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ w3o 1085 ∈ wcel 2106 ∀wral 3064 class class class wbr 5074 E cep 5494 Po wpo 5501 Or wor 5502 Fr wfr 5541 We wwe 5543 Ord word 6265 Oncon0 6266 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-tr 5192 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-ord 6269 df-on 6270 |
This theorem is referenced by: ordon 7627 omsinds 7733 omsindsOLD 7734 onnseq 8175 dfrecs3 8203 dfrecs3OLD 8204 tfr1ALT 8231 tfr2ALT 8232 tfr3ALT 8233 ordunifi 9064 ordtypelem8 9284 oismo 9299 cantnfcl 9425 leweon 9767 r0weon 9768 ac10ct 9790 dfac12lem2 9900 cflim2 10019 cofsmo 10025 hsmexlem1 10182 smobeth 10342 gruina 10574 ltsopi 10644 dford5 33671 on2recsfn 33826 on2recsov 33827 on2ind 33828 on3ind 33829 finminlem 34507 dnwech 40873 aomclem4 40882 |
Copyright terms: Public domain | W3C validator |