![]() |
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 7673, see epweonALT 7711. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7673. (Revised by BTernaryTau, 30-Nov-2024.) |
Ref | Expression |
---|---|
epweon | ⊢ E We On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onfr 6357 | . 2 ⊢ E Fr On | |
2 | df-po 5546 | . . . 4 ⊢ ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) | |
3 | eloni 6328 | . . . . . . . . 9 ⊢ (𝑥 ∈ On → Ord 𝑥) | |
4 | ordirr 6336 | . . . . . . . . 9 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥) | |
5 | 3, 4 | syl 17 | . . . . . . . 8 ⊢ (𝑥 ∈ On → ¬ 𝑥 ∈ 𝑥) |
6 | epel 5541 | . . . . . . . 8 ⊢ (𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥) | |
7 | 5, 6 | sylnibr 329 | . . . . . . 7 ⊢ (𝑥 ∈ On → ¬ 𝑥 E 𝑥) |
8 | ontr1 6364 | . . . . . . . 8 ⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) | |
9 | epel 5541 | . . . . . . . . 9 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) | |
10 | epel 5541 | . . . . . . . . 9 ⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧) | |
11 | 9, 10 | anbi12i 628 | . . . . . . . 8 ⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧)) |
12 | epel 5541 | . . . . . . . 8 ⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧) | |
13 | 8, 11, 12 | 3imtr4g 296 | . . . . . . 7 ⊢ (𝑧 ∈ On → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)) |
14 | 7, 13 | anim12i 614 | . . . . . 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 3072 | . . 3 ⊢ E Po On |
18 | eloni 6328 | . . . . 5 ⊢ (𝑦 ∈ On → Ord 𝑦) | |
19 | ordtri3or 6350 | . . . . . 6 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) | |
20 | biid 261 | . . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) | |
21 | epel 5541 | . . . . . . 7 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥) | |
22 | 9, 20, 21 | 3orbi123i 1157 | . . . . . 6 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
23 | 19, 22 | sylibr 233 | . . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
24 | 3, 18, 23 | syl2an 597 | . . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)) |
25 | 24 | rgen2 3195 | . . 3 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) |
26 | df-so 5547 | . . 3 ⊢ ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))) | |
27 | 17, 25, 26 | mpbir2an 710 | . 2 ⊢ E Or On |
28 | df-we 5591 | . 2 ⊢ ( E We On ↔ ( E Fr On ∧ E Or On)) | |
29 | 1, 27, 28 | mpbir2an 710 | 1 ⊢ E We On |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∨ w3o 1087 ∈ wcel 2107 ∀wral 3065 class class class wbr 5106 E cep 5537 Po wpo 5544 Or wor 5545 Fr wfr 5586 We wwe 5588 Ord word 6317 Oncon0 6318 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-ral 3066 df-rex 3075 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3930 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-tr 5224 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5589 df-we 5591 df-ord 6321 df-on 6322 |
This theorem is referenced by: ordon 7712 dford5 7719 omsinds 7824 omsindsOLD 7825 onnseq 8291 dfrecs3 8319 dfrecs3OLD 8320 tfr1ALT 8347 tfr2ALT 8348 tfr3ALT 8349 on2recsfn 8614 on2recsov 8615 on2ind 8616 on3ind 8617 ordunifi 9238 ordtypelem8 9462 oismo 9477 cantnfcl 9604 leweon 9948 r0weon 9949 ac10ct 9971 dfac12lem2 10081 cflim2 10200 cofsmo 10206 hsmexlem1 10363 smobeth 10523 gruina 10755 ltsopi 10825 finminlem 34793 dnwech 41378 aomclem4 41387 onsupuni 41566 oninfint 41573 epsoon 41590 epirron 41591 oneptr 41592 |
Copyright terms: Public domain | W3C validator |