Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  onfr Structured version   Visualization version   GIF version

Theorem onfr 6201
 Description: The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7485 (through epweon 7484) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994.)
Assertion
Ref Expression
onfr E Fr On

Proof of Theorem onfr
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfepfr 5505 . 2 ( E Fr On ↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅))
2 n0 4260 . . . 4 (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦𝑥)
3 ineq2 4133 . . . . . . . . . 10 (𝑧 = 𝑦 → (𝑥𝑧) = (𝑥𝑦))
43eqeq1d 2800 . . . . . . . . 9 (𝑧 = 𝑦 → ((𝑥𝑧) = ∅ ↔ (𝑥𝑦) = ∅))
54rspcev 3571 . . . . . . . 8 ((𝑦𝑥 ∧ (𝑥𝑦) = ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
65adantll 713 . . . . . . 7 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) = ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
7 inss1 4155 . . . . . . . 8 (𝑥𝑦) ⊆ 𝑥
8 ssel2 3910 . . . . . . . . . . 11 ((𝑥 ⊆ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
9 eloni 6172 . . . . . . . . . . 11 (𝑦 ∈ On → Ord 𝑦)
10 ordfr 6177 . . . . . . . . . . 11 (Ord 𝑦 → E Fr 𝑦)
118, 9, 103syl 18 . . . . . . . . . 10 ((𝑥 ⊆ On ∧ 𝑦𝑥) → E Fr 𝑦)
12 inss2 4156 . . . . . . . . . . 11 (𝑥𝑦) ⊆ 𝑦
13 vex 3444 . . . . . . . . . . . . 13 𝑥 ∈ V
1413inex1 5186 . . . . . . . . . . . 12 (𝑥𝑦) ∈ V
1514epfrc 5506 . . . . . . . . . . 11 (( E Fr 𝑦 ∧ (𝑥𝑦) ⊆ 𝑦 ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅)
1612, 15mp3an2 1446 . . . . . . . . . 10 (( E Fr 𝑦 ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅)
1711, 16sylan 583 . . . . . . . . 9 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅)
18 inass 4146 . . . . . . . . . . . . 13 ((𝑥𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦𝑧))
198, 9syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ⊆ On ∧ 𝑦𝑥) → Ord 𝑦)
20 elinel2 4123 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑥𝑦) → 𝑧𝑦)
21 ordelss 6178 . . . . . . . . . . . . . . . 16 ((Ord 𝑦𝑧𝑦) → 𝑧𝑦)
2219, 20, 21syl2an 598 . . . . . . . . . . . . . . 15 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → 𝑧𝑦)
23 sseqin2 4142 . . . . . . . . . . . . . . 15 (𝑧𝑦 ↔ (𝑦𝑧) = 𝑧)
2422, 23sylib 221 . . . . . . . . . . . . . 14 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → (𝑦𝑧) = 𝑧)
2524ineq2d 4139 . . . . . . . . . . . . 13 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → (𝑥 ∩ (𝑦𝑧)) = (𝑥𝑧))
2618, 25syl5eq 2845 . . . . . . . . . . . 12 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → ((𝑥𝑦) ∩ 𝑧) = (𝑥𝑧))
2726eqeq1d 2800 . . . . . . . . . . 11 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → (((𝑥𝑦) ∩ 𝑧) = ∅ ↔ (𝑥𝑧) = ∅))
2827rexbidva 3255 . . . . . . . . . 10 ((𝑥 ⊆ On ∧ 𝑦𝑥) → (∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅))
2928adantr 484 . . . . . . . . 9 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅))
3017, 29mpbid 235 . . . . . . . 8 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅)
31 ssrexv 3982 . . . . . . . 8 ((𝑥𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅ → ∃𝑧𝑥 (𝑥𝑧) = ∅))
327, 30, 31mpsyl 68 . . . . . . 7 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
336, 32pm2.61dane 3074 . . . . . 6 ((𝑥 ⊆ On ∧ 𝑦𝑥) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
3433ex 416 . . . . 5 (𝑥 ⊆ On → (𝑦𝑥 → ∃𝑧𝑥 (𝑥𝑧) = ∅))
3534exlimdv 1934 . . . 4 (𝑥 ⊆ On → (∃𝑦 𝑦𝑥 → ∃𝑧𝑥 (𝑥𝑧) = ∅))
362, 35syl5bi 245 . . 3 (𝑥 ⊆ On → (𝑥 ≠ ∅ → ∃𝑧𝑥 (𝑥𝑧) = ∅))
3736imp 410 . 2 ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
381, 37mpgbir 1801 1 E Fr On
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243   E cep 5430   Fr wfr 5476  Ord word 6161  Oncon0 6162 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5032  df-opab 5094  df-tr 5138  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-ord 6165  df-on 6166 This theorem is referenced by:  epweon  7484
 Copyright terms: Public domain W3C validator