Metamath Proof Explorer

Theorem unblem1

Description: Lemma for unbnn . 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)

Ref Expression
Assertion unblem1 
|- ( ( ( B C_ _om /\ A. x e. _om E. y e. B x e. y ) /\ A e. B ) -> |^| ( B \ suc A ) e. B )

Proof

Step Hyp Ref Expression
1 omsson 
 |-  _om C_ On
2 sstr 
 |-  ( ( B C_ _om /\ _om C_ On ) -> B C_ On )
3 1 2 mpan2 
 |-  ( B C_ _om -> B C_ On )
4 3 ssdifssd 
 |-  ( B C_ _om -> ( B \ suc A ) C_ On )
5 4 ad2antrr 
 |-  ( ( ( B C_ _om /\ A. x e. _om E. y e. B x e. y ) /\ A e. B ) -> ( B \ suc A ) C_ On )
6 ssel 
 |-  ( B C_ _om -> ( A e. B -> A e. _om ) )
7 peano2b 
 |-  ( A e. _om <-> suc A e. _om )
8 6 7 imbitrdi 
 |-  ( B C_ _om -> ( A e. B -> suc A e. _om ) )
9 eleq1 
 |-  ( x = suc A -> ( x e. y <-> suc A e. y ) )
10 9 rexbidv 
 |-  ( x = suc A -> ( E. y e. B x e. y <-> E. y e. B suc A e. y ) )
11 10 rspccva 
 |-  ( ( 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 
 |-  ( B C_ _om -> ( y e. B -> y e. _om ) )
13 nnord 
 |-  ( y e. _om -> Ord y )
14 ordn2lp 
 |-  ( Ord y -> -. ( y e. suc A /\ suc A e. y ) )
15 imnan 
 |-  ( ( y e. suc A -> -. suc A e. y ) <-> -. ( y e. suc A /\ suc A e. y ) )
16 14 15 sylibr 
 |-  ( Ord y -> ( y e. suc A -> -. suc A e. y ) )
17 16 con2d 
 |-  ( Ord y -> ( suc A e. y -> -. y e. suc A ) )
18 13 17 syl 
 |-  ( y e. _om -> ( suc A e. y -> -. y e. suc A ) )
19 12 18 syl6 
 |-  ( B C_ _om -> ( y e. B -> ( suc A e. y -> -. y e. suc A ) ) )
20 19 imdistand 
 |-  ( B C_ _om -> ( ( y e. B /\ suc A e. y ) -> ( y e. B /\ -. y e. suc A ) ) )
21 eldif 
 |-  ( y e. ( B \ suc A ) <-> ( y e. B /\ -. y e. suc A ) )
22 ne0i 
 |-  ( y e. ( B \ suc A ) -> ( B \ suc A ) =/= (/) )
23 21 22 sylbir 
 |-  ( ( y e. B /\ -. y e. suc A ) -> ( B \ suc A ) =/= (/) )
24 20 23 syl6 
 |-  ( B C_ _om -> ( ( y e. B /\ suc A e. y ) -> ( B \ suc A ) =/= (/) ) )
25 24 expd 
 |-  ( B C_ _om -> ( y e. B -> ( suc A e. y -> ( B \ suc A ) =/= (/) ) ) )
26 25 rexlimdv 
 |-  ( B C_ _om -> ( E. y e. B suc A e. y -> ( B \ suc A ) =/= (/) ) )
27 11 26 syl5 
 |-  ( 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 
 |-  ( B C_ _om -> ( ( A. x e. _om E. y e. B x e. y /\ A e. B ) -> ( B \ suc A ) =/= (/) ) )
29 28 impl 
 |-  ( ( ( B C_ _om /\ A. x e. _om E. y e. B x e. y ) /\ A e. B ) -> ( B \ suc A ) =/= (/) )
30 onint 
 |-  ( ( ( B \ suc A ) C_ On /\ ( B \ suc A ) =/= (/) ) -> |^| ( B \ suc A ) e. ( B \ suc A ) )
31 5 29 30 syl2anc 
 |-  ( ( ( 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 
 |-  ( ( ( B C_ _om /\ A. x e. _om E. y e. B x e. y ) /\ A e. B ) -> |^| ( B \ suc A ) e. B )