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

Theorem onint 7809
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 7795 . . . 4 Ord On
2 tz7.5 6406 . . . 4 ((Ord On ∧ 𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴 (𝐴𝑥) = ∅)
31, 2mp3an1 1447 . . 3 ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴 (𝐴𝑥) = ∅)
4 ssel 3988 . . . . . . . . . . . . . . . 16 (𝐴 ⊆ On → (𝑥𝐴𝑥 ∈ On))
54imdistani 568 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ On ∧ 𝑥𝐴) → (𝐴 ⊆ On ∧ 𝑥 ∈ On))
6 ssel 3988 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ⊆ On → (𝑧𝐴𝑧 ∈ On))
7 ontri1 6419 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑥𝑧 ↔ ¬ 𝑧𝑥))
8 ssel 3988 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑧 → (𝑦𝑥𝑦𝑧))
97, 8biimtrrdi 254 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧𝑥 → (𝑦𝑥𝑦𝑧)))
109ex 412 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → (𝑧 ∈ On → (¬ 𝑧𝑥 → (𝑦𝑥𝑦𝑧))))
116, 10sylan9 507 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧𝐴 → (¬ 𝑧𝑥 → (𝑦𝑥𝑦𝑧))))
1211com4r 94 . . . . . . . . . . . . . . . . . 18 (𝑦𝑥 → ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧𝐴 → (¬ 𝑧𝑥𝑦𝑧))))
1312imp31 417 . . . . . . . . . . . . . . . . 17 (((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) ∧ 𝑧𝐴) → (¬ 𝑧𝑥𝑦𝑧))
1413ralimdva 3164 . . . . . . . . . . . . . . . 16 ((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → (∀𝑧𝐴 ¬ 𝑧𝑥 → ∀𝑧𝐴 𝑦𝑧))
15 disj 4455 . . . . . . . . . . . . . . . 16 ((𝐴𝑥) = ∅ ↔ ∀𝑧𝐴 ¬ 𝑧𝑥)
16 vex 3481 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
1716elint2 4957 . . . . . . . . . . . . . . . 16 (𝑦 𝐴 ↔ ∀𝑧𝐴 𝑦𝑧)
1814, 15, 173imtr4g 296 . . . . . . . . . . . . . . 15 ((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → ((𝐴𝑥) = ∅ → 𝑦 𝐴))
195, 18sylan2 593 . . . . . . . . . . . . . 14 ((𝑦𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥𝐴)) → ((𝐴𝑥) = ∅ → 𝑦 𝐴))
2019exp32 420 . . . . . . . . . . . . 13 (𝑦𝑥 → (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → 𝑦 𝐴))))
2120com4l 92 . . . . . . . . . . . 12 (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → (𝑦𝑥𝑦 𝐴))))
2221imp32 418 . . . . . . . . . . 11 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → (𝑦𝑥𝑦 𝐴))
2322ssrdv 4000 . . . . . . . . . 10 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → 𝑥 𝐴)
24 intss1 4967 . . . . . . . . . . 11 (𝑥𝐴 𝐴𝑥)
2524ad2antrl 728 . . . . . . . . . 10 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → 𝐴𝑥)
2623, 25eqssd 4012 . . . . . . . . 9 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → 𝑥 = 𝐴)
2726eleq1d 2823 . . . . . . . 8 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → (𝑥𝐴 𝐴𝐴))
2827biimpd 229 . . . . . . 7 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ (𝐴𝑥) = ∅)) → (𝑥𝐴 𝐴𝐴))
2928exp32 420 . . . . . 6 (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → (𝑥𝐴 𝐴𝐴))))
3029com34 91 . . . . 5 (𝐴 ⊆ On → (𝑥𝐴 → (𝑥𝐴 → ((𝐴𝑥) = ∅ → 𝐴𝐴))))
3130pm2.43d 53 . . . 4 (𝐴 ⊆ On → (𝑥𝐴 → ((𝐴𝑥) = ∅ → 𝐴𝐴)))
3231rexlimdv 3150 . . 3 (𝐴 ⊆ On → (∃𝑥𝐴 (𝐴𝑥) = ∅ → 𝐴𝐴))
333, 32syl5 34 . 2 (𝐴 ⊆ On → ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → 𝐴𝐴))
3433anabsi5 669 1 ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → 𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  cin 3961  wss 3962  c0 4338   cint 4950  Ord word 6384  Oncon0 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389
This theorem is referenced by:  onint0  7810  onssmin  7811  onminesb  7812  onminsb  7813  oninton  7814  oneqmin  7819  oeeulem  8637  nnawordex  8673  unblem1  9325  unblem2  9326  tz9.12lem3  9826  scott0  9923  cardid2  9990  ackbij1lem18  10273  cardcf  10289  cff1  10295  cflim2  10300  cfss  10302  cofsmo  10306  fin23lem26  10362  pwfseqlem3  10697  gruina  10855  2ndcdisj  23479  sltval2  27715  nocvxmin  27837  lrrecfr  27990  rankeq1o  36152  dnnumch3  43035  oninfint  43224  inaex  44292
  Copyright terms: Public domain W3C validator