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

Step	Hyp	Ref	Expression
1		omsson 6701	. . . . . 6 |- om C_ On
2		sstr 3469	. . . . . 6 |- ( ( B C_ om /\ om C_ On ) -> B C_ On )
3	1, 2	mpan2 675	. . . . 5 |- ( B C_ om -> B C_ On )
4	3	ssdifssd 3600	. . . 4 |- ( B C_ om -> ( B \ suc A ) C_ On )
5	4	ad2antrr 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 )
8	6, 7	syl6ib 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 ) )
10	9	rexbidv 2937	. . . . . . 7 |- ( x = suc A -> ( E. y e. B x e. y <-> E. y e. B suc A e. y ) )
11	10	rspccva 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 ) )
16	14, 15	sylibr 215	. . . . . . . . . . . . 13 |- ( Ord y -> ( y e. suc A -> -. suc A e. y ) )
17	16	con2d 118	. . . . . . . . . . . 12 |- ( Ord y -> ( suc A e. y -> -. y e. suc A ) )
18	13, 17	syl 17	. . . . . . . . . . 11 |- ( y e. om -> ( suc A e. y -> -. y e. suc A ) )
19	12, 18	syl6 34	. . . . . . . . . 10 |- ( B C_ om -> ( y e. B -> ( suc A e. y -> -. y e. suc A ) ) )
20	19	imdistand 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 ) =/= (/) )
23	21, 22	sylbir 216	. . . . . . . . 9 |- ( ( y e. B /\ -. y e. suc A ) -> ( B \ suc A ) =/= (/) )
24	20, 23	syl6 34	. . . . . . . 8 |- ( B C_ om -> ( ( y e. B /\ suc A e. y ) -> ( B \ suc A ) =/= (/) ) )
25	24	expd 437	. . . . . . 7 |- ( B C_ om -> ( y e. B -> ( suc A e. y -> ( B \ suc A ) =/= (/) ) ) )
26	25	rexlimdv 2913	. . . . . 6 |- ( B C_ om -> ( E. y e. B suc A e. y -> ( B \ suc A ) =/= (/) ) )
27	11, 26	syl5 33	. . . . 5 |- ( B C_ om -> ( ( A. x e. om E. y e. B x e. y /\ suc A e. om ) -> ( B \ suc A ) =/= (/) ) )
28	8, 27	sylan2d 484	. . . 4 |- ( B C_ om -> ( ( A. x e. om E. y e. B x e. y /\ A e. B ) -> ( B \ suc A ) =/= (/) ) )
29	28	impl 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 ) )
31	5, 29, 30	syl2anc 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 ) )
32	31	eldifad 3445	1 |- ( ( ( B C_ om /\ A. x e. om E. y e. B x e. y ) /\ A e. B ) -> |^| ( B \ suc A ) e. B )

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