MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unblem1 Structured version   Unicode version

Theorem unblem1 7820
Description: Lemma for unbnn 7824. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003.)
Assertion
Ref Expression
unblem1  |-  ( ( ( B  C_  om  /\  A. x  e.  om  E. y  e.  B  x  e.  y )  /\  A  e.  B )  ->  |^| ( B  \  suc  A )  e.  B )
Distinct variable groups:    x, y, A    x, B, y

Proof of Theorem unblem1
StepHypRef Expression
1 omsson 6701 . . . . . 6  |-  om  C_  On
2 sstr 3469 . . . . . 6  |-  ( ( B  C_  om  /\  om  C_  On )  ->  B  C_  On )
31, 2mpan2 675 . . . . 5  |-  ( B 
C_  om  ->  B  C_  On )
43ssdifssd 3600 . . . 4  |-  ( B 
C_  om  ->  ( B 
\  suc  A )  C_  On )
54ad2antrr 730 . . 3  |-  ( ( ( B  C_  om  /\  A. x  e.  om  E. y  e.  B  x  e.  y )  /\  A  e.  B )  ->  ( B  \  suc  A ) 
C_  On )
6 ssel 3455 . . . . . 6  |-  ( B 
C_  om  ->  ( A  e.  B  ->  A  e.  om ) )
7 peano2b 6713 . . . . . 6  |-  ( A  e.  om  <->  suc  A  e. 
om )
86, 7syl6ib 229 . . . . 5  |-  ( B 
C_  om  ->  ( A  e.  B  ->  suc  A  e.  om ) )
9 eleq1 2492 . . . . . . . 8  |-  ( x  =  suc  A  -> 
( x  e.  y  <->  suc  A  e.  y ) )
109rexbidv 2937 . . . . . . 7  |-  ( x  =  suc  A  -> 
( E. y  e.  B  x  e.  y  <->  E. y  e.  B  suc  A  e.  y ) )
1110rspccva 3178 . . . . . 6  |-  ( ( A. x  e.  om  E. y  e.  B  x  e.  y  /\  suc  A  e.  om )  ->  E. y  e.  B  suc  A  e.  y )
12 ssel 3455 . . . . . . . . . . 11  |-  ( B 
C_  om  ->  ( y  e.  B  ->  y  e.  om ) )
13 nnord 6705 . . . . . . . . . . . 12  |-  ( y  e.  om  ->  Ord  y )
14 ordn2lp 5453 . . . . . . . . . . . . . 14  |-  ( Ord  y  ->  -.  (
y  e.  suc  A  /\  suc  A  e.  y ) )
15 imnan 423 . . . . . . . . . . . . . 14  |-  ( ( y  e.  suc  A  ->  -.  suc  A  e.  y )  <->  -.  (
y  e.  suc  A  /\  suc  A  e.  y ) )
1614, 15sylibr 215 . . . . . . . . . . . . 13  |-  ( Ord  y  ->  ( y  e.  suc  A  ->  -.  suc  A  e.  y ) )
1716con2d 118 . . . . . . . . . . . 12  |-  ( Ord  y  ->  ( suc  A  e.  y  ->  -.  y  e.  suc  A ) )
1813, 17syl 17 . . . . . . . . . . 11  |-  ( y  e.  om  ->  ( suc  A  e.  y  ->  -.  y  e.  suc  A ) )
1912, 18syl6 34 . . . . . . . . . 10  |-  ( B 
C_  om  ->  ( y  e.  B  ->  ( suc  A  e.  y  ->  -.  y  e.  suc  A ) ) )
2019imdistand 696 . . . . . . . . 9  |-  ( B 
C_  om  ->  ( ( y  e.  B  /\  suc  A  e.  y )  ->  ( y  e.  B  /\  -.  y  e.  suc  A ) ) )
21 eldif 3443 . . . . . . . . . 10  |-  ( y  e.  ( B  \  suc  A )  <->  ( y  e.  B  /\  -.  y  e.  suc  A ) )
22 ne0i 3764 . . . . . . . . . 10  |-  ( y  e.  ( B  \  suc  A )  ->  ( B  \  suc  A )  =/=  (/) )
2321, 22sylbir 216 . . . . . . . . 9  |-  ( ( y  e.  B  /\  -.  y  e.  suc  A )  ->  ( B  \  suc  A )  =/=  (/) )
2420, 23syl6 34 . . . . . . . 8  |-  ( B 
C_  om  ->  ( ( y  e.  B  /\  suc  A  e.  y )  ->  ( B  \  suc  A )  =/=  (/) ) )
2524expd 437 . . . . . . 7  |-  ( B 
C_  om  ->  ( y  e.  B  ->  ( suc  A  e.  y  -> 
( B  \  suc  A )  =/=  (/) ) ) )
2625rexlimdv 2913 . . . . . 6  |-  ( B 
C_  om  ->  ( E. y  e.  B  suc  A  e.  y  ->  ( B  \  suc  A )  =/=  (/) ) )
2711, 26syl5 33 . . . . 5  |-  ( B 
C_  om  ->  ( ( A. x  e.  om  E. y  e.  B  x  e.  y  /\  suc  A  e.  om )  -> 
( B  \  suc  A )  =/=  (/) ) )
288, 27sylan2d 484 . . . 4  |-  ( B 
C_  om  ->  ( ( A. x  e.  om  E. y  e.  B  x  e.  y  /\  A  e.  B )  ->  ( B  \  suc  A )  =/=  (/) ) )
2928impl 624 . . 3  |-  ( ( ( B  C_  om  /\  A. x  e.  om  E. y  e.  B  x  e.  y )  /\  A  e.  B )  ->  ( B  \  suc  A )  =/=  (/) )
30 onint 6627 . . 3  |-  ( ( ( B  \  suc  A )  C_  On  /\  ( B  \  suc  A )  =/=  (/) )  ->  |^| ( B  \  suc  A )  e.  ( B  \  suc  A ) )
315, 29, 30syl2anc 665 . 2  |-  ( ( ( B  C_  om  /\  A. x  e.  om  E. y  e.  B  x  e.  y )  /\  A  e.  B )  ->  |^| ( B  \  suc  A )  e.  ( B  \  suc  A ) )
3231eldifad 3445 1  |-  ( ( ( B  C_  om  /\  A. x  e.  om  E. y  e.  B  x  e.  y )  /\  A  e.  B )  ->  |^| ( B  \  suc  A )  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1867    =/= wne 2616   A.wral 2773   E.wrex 2774    \ cdif 3430    C_ wss 3433   (/)c0 3758   |^|cint 4249   Ord word 5432   Oncon0 5433   suc csuc 5435   omcom 6697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652  ax-un 6588
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-br 4418  df-opab 4476  df-tr 4512  df-eprel 4756  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-om 6698
This theorem is referenced by:  unblem2  7821  unblem3  7822
  Copyright terms: Public domain W3C validator