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

Theorem onint 7730
Description: The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.)
Assertion
Ref Expression
onint ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → 𝐴𝐴)

Proof of Theorem onint
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordon 7716 . . . 4 Ord On
2 tz7.5 6343 . . . 4 ((Ord On ∧ 𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴 (𝐴𝑥) = ∅)
31, 2mp3an1 1449 . . 3 ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴 (𝐴𝑥) = ∅)
4 ssel 3942 . . . . . . . . . . . . . . . 16 (𝐴 ⊆ On → (𝑥𝐴𝑥 ∈ On))
54imdistani 570 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ On ∧ 𝑥𝐴) → (𝐴 ⊆ On ∧ 𝑥 ∈ On))
6 ssel 3942 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ⊆ On → (𝑧𝐴𝑧 ∈ On))
7 ontri1 6356 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑥𝑧 ↔ ¬ 𝑧𝑥))
8 ssel 3942 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑧 → (𝑦𝑥𝑦𝑧))
97, 8syl6bir 254 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧𝑥 → (𝑦𝑥𝑦𝑧)))
109ex 414 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → (𝑧 ∈ On → (¬ 𝑧𝑥 → (𝑦𝑥𝑦𝑧))))
116, 10sylan9 509 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧𝐴 → (¬ 𝑧𝑥 → (𝑦𝑥𝑦𝑧))))
1211com4r 94 . . . . . . . . . . . . . . . . . 18 (𝑦𝑥 → ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧𝐴 → (¬ 𝑧𝑥𝑦𝑧))))
1312imp31 419 . . . . . . . . . . . . . . . . 17 (((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) ∧ 𝑧𝐴) → (¬ 𝑧𝑥𝑦𝑧))
1413ralimdva 3165 . . . . . . . . . . . . . . . 16 ((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → (∀𝑧𝐴 ¬ 𝑧𝑥 → ∀𝑧𝐴 𝑦𝑧))
15 disj 4412 . . . . . . . . . . . . . . . 16 ((𝐴𝑥) = ∅ ↔ ∀𝑧𝐴 ¬ 𝑧𝑥)
16 vex 3452 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
1716elint2 4919 . . . . . . . . . . . . . . . 16 (𝑦 𝐴 ↔ ∀𝑧𝐴 𝑦𝑧)
1814, 15, 173imtr4g 296 . . . . . . . . . . . . . . 15 ((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → ((𝐴𝑥) = ∅ → 𝑦 𝐴))
195, 18sylan2 594 . . . . . . . . . . . . . 14 ((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥𝐴)) → ((𝐴𝑥) = ∅ → 𝑦 𝐴))
2019exp32 422 . . . . . . . . . . . . 13 (𝑦𝑥 → (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → 𝑦 𝐴))))
2120com4l 92 . . . . . . . . . . . 12 (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → (𝑦𝑥𝑦 𝐴))))
2221imp32 420 . . . . . . . . . . 11 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → (𝑦𝑥𝑦 𝐴))
2322ssrdv 3955 . . . . . . . . . 10 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → 𝑥 𝐴)
24 intss1 4929 . . . . . . . . . . 11 (𝑥𝐴 𝐴𝑥)
2524ad2antrl 727 . . . . . . . . . 10 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → 𝐴𝑥)
2623, 25eqssd 3966 . . . . . . . . 9 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → 𝑥 = 𝐴)
2726eleq1d 2823 . . . . . . . 8 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → (𝑥𝐴 𝐴𝐴))
2827biimpd 228 . . . . . . 7 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → (𝑥𝐴 𝐴𝐴))
2928exp32 422 . . . . . 6 (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → (𝑥𝐴 𝐴𝐴))))
3029com34 91 . . . . 5 (𝐴 ⊆ On → (𝑥𝐴 → (𝑥𝐴 → ((𝐴𝑥) = ∅ → 𝐴𝐴))))
3130pm2.43d 53 . . . 4 (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → 𝐴𝐴)))
3231rexlimdv 3151 . . 3 (𝐴 ⊆ On → (∃𝑥𝐴 (𝐴𝑥) = ∅ → 𝐴𝐴))
333, 32syl5 34 . 2 (𝐴 ⊆ On → ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → 𝐴𝐴))
3433anabsi5 668 1 ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → 𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wcel 2107  wne 2944  wral 3065  wrex 3074  cin 3914  wss 3915  c0 4287   cint 4912  Ord word 6321  Oncon0 6322
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 5261  ax-nul 5268  ax-pr 5389
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 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-br 5111  df-opab 5173  df-tr 5228  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-ord 6325  df-on 6326
This theorem is referenced by:  onint0  7731  onssmin  7732  onminesb  7733  onminsb  7734  oninton  7735  oneqmin  7740  oeeulem  8553  nnawordex  8589  unblem1  9246  unblem2  9247  tz9.12lem3  9732  scott0  9829  cardid2  9896  ackbij1lem18  10180  cardcf  10195  cff1  10201  cflim2  10206  cfss  10208  cofsmo  10212  fin23lem26  10268  pwfseqlem3  10603  gruina  10761  2ndcdisj  22823  sltval2  27020  nocvxmin  27140  lrrecfr  27277  rankeq1o  34785  dnnumch3  41403  oninfint  41599  inaex  42651
  Copyright terms: Public domain W3C validator