Theorem epweon 7725

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 7685, see epweonALT 7726. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7685. (Revised by BTernaryTau, 30-Nov-2024.)

Assertion

Ref	Expression
epweon	⊢ E We On

Proof of Theorem epweon

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		onfr 6356	. 2 ⊢ E Fr On
2		df-po 5533	. . . 4 ⊢ ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
3		eloni 6327	. . . . . . . . 9 ⊢ (𝑥 ∈ On → Ord 𝑥)
4		ordirr 6335	. . . . . . . . 9 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ On → ¬ 𝑥 ∈ 𝑥)
6		epel 5528	. . . . . . . 8 ⊢ (𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥)
7	5, 6	sylnibr 330	. . . . . . 7 ⊢ (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8		ontr1 6364	. . . . . . . 8 ⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
9		epel 5528	. . . . . . . . 9 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)
10		epel 5528	. . . . . . . . 9 ⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧)
11	9, 10	anbi12i 634	. . . . . . . 8 ⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧))
12		epel 5528	. . . . . . . 8 ⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧)
13	8, 11, 12	3imtr4g 297	. . . . . . 7 ⊢ (𝑧 ∈ On → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))
14	7, 13	anim12i 619	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
15	14	ralrimiva 3132	. . . . 5 ⊢ (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
16	15	ralrimivw 3136	. . . 4 ⊢ (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
17	2, 16	mprgbir 3061	. . 3 ⊢ E Po On
18		eloni 6327	. . . . 5 ⊢ (𝑦 ∈ On → Ord 𝑦)
19		ordtri3or 6349	. . . . . 6 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
20		biid 262	. . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦)
21		epel 5528	. . . . . . 7 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥)
22	9, 20, 21	3orbi123i 1162	. . . . . 6 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
23	19, 22	sylibr 235	. . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))
24	3, 18, 23	syl2an 602	. . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))
25	24	rgen2 3180	. . 3 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)
26		df-so 5534	. . 3 ⊢ ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)))
27	17, 25, 26	mpbir2an 717	. 2 ⊢ E Or On
28		df-we 5580	. 2 ⊢ ( E We On ↔ ( E Fr On ∧ E Or On))
29	1, 27, 28	mpbir2an 717	1 ⊢ E We On

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ w3o 1091   ∈ wcel 2119  ∀wral 3054   class class class wbr 5079   E cep 5524   Po wpo 5531   Or wor 5532   Fr wfr 5575   We wwe 5577  Ord word 6316  Oncon0 6317

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5187  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321

This theorem is referenced by:  ordon  7727  dford5  7734  omsinds  7834  onnseq  8281  dfrecs3  8309  tfr1ALT  8336  tfr2ALT  8337  tfr3ALT  8338  on2recsfn  8600  on2recsov  8601  on2ind  8602  on3ind  8603  ordunifi  9197  ordtypelem8  9437  oismo  9452  cantnfcl  9586  leweon  9931  r0weon  9932  ac10ct  9954  dfac12lem2  10065  cflim2  10183  cofsmo  10189  hsmexlem1  10346  smobeth  10507  gruina  10739  ltsopi  10809  onswe  28289  finminlem  36553  dnwech  43500  aomclem4  43509  onsupuni  43681  oninfint  43688  epsoon  43705  epirron  43706  oneptr  43707  oaun3lem1  43826