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 ω x ω y B x y A B B suc A B

Proof

Step Hyp Ref Expression
1 omsson ω On
2 sstr B ω ω On B On
3 1 2 mpan2 B ω B On
4 3 ssdifssd B ω B suc A On
5 4 ad2antrr B ω x ω y B x y A B B suc A On
6 ssel B ω A B A ω
7 peano2b A ω suc A ω
8 6 7 syl6ib B ω A B suc A ω
9 eleq1 x = suc A x y suc A y
10 9 rexbidv x = suc A y B x y y B suc A y
11 10 rspccva x ω y B x y suc A ω y B suc A y
12 ssel B ω y B y ω
13 nnord y ω Ord y
14 ordn2lp Ord y ¬ y suc A suc A y
15 imnan y suc A ¬ suc A y ¬ y suc A suc A y
16 14 15 sylibr Ord y y suc A ¬ suc A y
17 16 con2d Ord y suc A y ¬ y suc A
18 13 17 syl y ω suc A y ¬ y suc A
19 12 18 syl6 B ω y B suc A y ¬ y suc A
20 19 imdistand B ω y B suc A y y B ¬ y suc A
21 eldif y B suc A y B ¬ y suc A
22 ne0i y B suc A B suc A
23 21 22 sylbir y B ¬ y suc A B suc A
24 20 23 syl6 B ω y B suc A y B suc A
25 24 expd B ω y B suc A y B suc A
26 25 rexlimdv B ω y B suc A y B suc A
27 11 26 syl5 B ω x ω y B x y suc A ω B suc A
28 8 27 sylan2d B ω x ω y B x y A B B suc A
29 28 impl B ω x ω y B x y A B B suc A
30 onint B suc A On B suc A B suc A B suc A
31 5 29 30 syl2anc B ω x ω y B x y A B B suc A B suc A
32 31 eldifad B ω x ω y B x y A B B suc A B