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

Theorem onfr 6356
Description: The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7711 (through epweon 7709) 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 5618 . 2 ( E Fr On ↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅))
2 n0 4306 . . . 4 (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦𝑥)
3 ineq2 4166 . . . . . . . . . 10 (𝑧 = 𝑦 → (𝑥𝑧) = (𝑥𝑦))
43eqeq1d 2738 . . . . . . . . 9 (𝑧 = 𝑦 → ((𝑥𝑧) = ∅ ↔ (𝑥𝑦) = ∅))
54rspcev 3581 . . . . . . . 8 ((𝑦𝑥 ∧ (𝑥𝑦) = ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
65adantll 712 . . . . . . 7 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) = ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
7 inss1 4188 . . . . . . . 8 (𝑥𝑦) ⊆ 𝑥
8 ssel2 3939 . . . . . . . . . . 11 ((𝑥 ⊆ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
9 eloni 6327 . . . . . . . . . . 11 (𝑦 ∈ On → Ord 𝑦)
10 ordfr 6332 . . . . . . . . . . 11 (Ord 𝑦 → E Fr 𝑦)
118, 9, 103syl 18 . . . . . . . . . 10 ((𝑥 ⊆ On ∧ 𝑦𝑥) → E Fr 𝑦)
12 inss2 4189 . . . . . . . . . . 11 (𝑥𝑦) ⊆ 𝑦
13 vex 3449 . . . . . . . . . . . . 13 𝑥 ∈ V
1413inex1 5274 . . . . . . . . . . . 12 (𝑥𝑦) ∈ V
1514epfrc 5619 . . . . . . . . . . 11 (( E Fr 𝑦 ∧ (𝑥𝑦) ⊆ 𝑦 ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅)
1612, 15mp3an2 1449 . . . . . . . . . 10 (( E Fr 𝑦 ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅)
1711, 16sylan 580 . . . . . . . . 9 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅)
18 inass 4179 . . . . . . . . . . . . 13 ((𝑥𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦𝑧))
198, 9syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ⊆ On ∧ 𝑦𝑥) → Ord 𝑦)
20 elinel2 4156 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑥𝑦) → 𝑧𝑦)
21 ordelss 6333 . . . . . . . . . . . . . . . 16 ((Ord 𝑦𝑧𝑦) → 𝑧𝑦)
2219, 20, 21syl2an 596 . . . . . . . . . . . . . . 15 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → 𝑧𝑦)
23 sseqin2 4175 . . . . . . . . . . . . . . 15 (𝑧𝑦 ↔ (𝑦𝑧) = 𝑧)
2422, 23sylib 217 . . . . . . . . . . . . . 14 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → (𝑦𝑧) = 𝑧)
2524ineq2d 4172 . . . . . . . . . . . . 13 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → (𝑥 ∩ (𝑦𝑧)) = (𝑥𝑧))
2618, 25eqtrid 2788 . . . . . . . . . . . 12 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → ((𝑥𝑦) ∩ 𝑧) = (𝑥𝑧))
2726eqeq1d 2738 . . . . . . . . . . 11 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ 𝑧 ∈ (𝑥𝑦)) → (((𝑥𝑦) ∩ 𝑧) = ∅ ↔ (𝑥𝑧) = ∅))
2827rexbidva 3173 . . . . . . . . . 10 ((𝑥 ⊆ On ∧ 𝑦𝑥) → (∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅))
2928adantr 481 . . . . . . . . 9 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥𝑦)((𝑥𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅))
3017, 29mpbid 231 . . . . . . . 8 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅)
31 ssrexv 4011 . . . . . . . 8 ((𝑥𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥𝑦)(𝑥𝑧) = ∅ → ∃𝑧𝑥 (𝑥𝑧) = ∅))
327, 30, 31mpsyl 68 . . . . . . 7 (((𝑥 ⊆ On ∧ 𝑦𝑥) ∧ (𝑥𝑦) ≠ ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
336, 32pm2.61dane 3032 . . . . . 6 ((𝑥 ⊆ On ∧ 𝑦𝑥) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
3433ex 413 . . . . 5 (𝑥 ⊆ On → (𝑦𝑥 → ∃𝑧𝑥 (𝑥𝑧) = ∅))
3534exlimdv 1936 . . . 4 (𝑥 ⊆ On → (∃𝑦 𝑦𝑥 → ∃𝑧𝑥 (𝑥𝑧) = ∅))
362, 35biimtrid 241 . . 3 (𝑥 ⊆ On → (𝑥 ≠ ∅ → ∃𝑧𝑥 (𝑥𝑧) = ∅))
3736imp 407 . 2 ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧𝑥 (𝑥𝑧) = ∅)
381, 37mpgbir 1801 1 E Fr On
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wne 2943  wrex 3073  cin 3909  wss 3910  c0 4282   E cep 5536   Fr wfr 5585  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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-tr 5223  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-ord 6320  df-on 6321
This theorem is referenced by:  epweon  7709  epweonALT  7710  on2recsfn  8613  on2recsov  8614  on2ind  8615  on3ind  8616
  Copyright terms: Public domain W3C validator