Theorem unblem1 4523

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

Assertion

Ref	Expression
unblem1	|- (((B (_ 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 3131	. . . . . 6 |- om (_ On
2		sstr 2068	. . . . . 6 |- ((B (_ om /\ om (_ On) -> B (_ On)
3	1, 2	mpan2 695	. . . . 5 |- (B (_ om -> B (_ On)
4		ssdifss 2164	. . . . 5 |- (B (_ On -> (B \ suc A) (_ On)
5	3, 4	syl 10	. . . 4 |- (B (_ om -> (B \ suc A) (_ On)
6	5	ad2antrr 404	. . 3 |- (((B (_ om /\ A.x e. om E.y e. B x e. y) /\ A e. B) -> (B \ suc A) (_ On)
7		ssel 2059	. . . . . . . . . . . 12 |- (B (_ om -> (y e. B -> y e. om))
8		nnord 3135	. . . . . . . . . . . . 13 |- (y e. om -> Ord y)
9		ordn2lp 2963	. . . . . . . . . . . . . . 15 |- (Ord y -> -. (y e. suc A /\ suc A e. y))
10		imnan 242	. . . . . . . . . . . . . . 15 |- ((y e. suc A -> -. suc A e. y) <-> -. (y e. suc A /\ suc A e. y))
11	9, 10	sylibr 200	. . . . . . . . . . . . . 14 |- (Ord y -> (y e. suc A -> -. suc A e. y))
12	11	con2d 91	. . . . . . . . . . . . 13 |- (Ord y -> (suc A e. y -> -. y e. suc A))
13	8, 12	syl 10	. . . . . . . . . . . 12 |- (y e. om -> (suc A e. y -> -. y e. suc A))
14	7, 13	syl6 22	. . . . . . . . . . 11 |- (B (_ om -> (y e. B -> (suc A e. y -> -. y e. suc A)))
15	14	imdistand 445	. . . . . . . . . 10 |- (B (_ om -> ((y e. B /\ suc A e. y) -> (y e. B /\ -. y e. suc A)))
16		eldif 2053	. . . . . . . . . . 11 |- (y e. (B \ suc A) <-> (y e. B /\ -. y e. suc A))
17		ne0i 2282	. . . . . . . . . . 11 |- (y e. (B \ suc A) -> (B \ suc A) =/= (/))
18	16, 17	sylbir 201	. . . . . . . . . 10 |- ((y e. B /\ -. y e. suc A) -> (B \ suc A) =/= (/))
19	15, 18	syl6 22	. . . . . . . . 9 |- (B (_ om -> ((y e. B /\ suc A e. y) -> (B \ suc A) =/= (/)))
20	19	exp3a 375	. . . . . . . 8 |- (B (_ om -> (y e. B -> (suc A e. y -> (B \ suc A) =/= (/))))
21	20	r19.23adv 1743	. . . . . . 7 |- (B (_ om -> (E.y e. B suc A e. y -> (B \ suc A) =/= (/)))
22		eleq1 1531	. . . . . . . . 9 |- (x = suc A -> (x e. y <-> suc A e. y))
23	22	rexbidv 1661	. . . . . . . 8 |- (x = suc A -> (E.y e. B x e. y <-> E.y e. B suc A e. y))
24	23	rcla4cva 1872	. . . . . . 7 |- ((A.x e. om E.y e. B x e. y /\ suc A e. om) -> E.y e. B suc A e. y)
25	21, 24	syl5 21	. . . . . 6 |- (B (_ om -> ((A.x e. om E.y e. B x e. y /\ suc A e. om) -> (B \ suc A) =/= (/)))
26		ssel 2059	. . . . . . 7 |- (B (_ om -> (A e. B -> A e. om))
27		peano2b 3142	. . . . . . 7 |- (A e. om <-> suc A e. om)
28	26, 27	syl6ib 212	. . . . . 6 |- (B (_ om -> (A e. B -> suc A e. om))
29	25, 28	sylan2d 458	. . . . 5 |- (B (_ om -> ((A.x e. om E.y e. B x e. y /\ A e. B) -> (B \ suc A) =/= (/)))
30	29	exp3a 375	. . . 4 |- (B (_ om -> (A.x e. om E.y e. B x e. y -> (A e. B -> (B \ suc A) =/= (/))))
31	30	imp31 362	. . 3 |- (((B (_ om /\ A.x e. om E.y e. B x e. y) /\ A e. B) -> (B \ suc A) =/= (/))
32	6, 31	jca 288	. 2 |- (((B (_ om /\ A.x e. om E.y e. B x e. y) /\ A e. B) -> ((B \ suc A) (_ On /\ (B \ suc A) =/= (/)))
33		onint 3001	. 2 |- (((B \ suc A) (_ On /\ (B \ suc A) =/= (/)) -> |^|(B \ suc A) e. (B \ suc A))
34		eldifi 2158	. 2 |- (|^|(B \ suc A) e. (B \ suc A) -> |^|(B \ suc A) e. B)
35	32, 33, 34	3syl 20	1 |- (((B (_ om /\ A.x e. om E.y e. B x e. y) /\ A e. B) -> |^|(B \ suc A) e. B)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 954   e. wcel 956   =/= wne 1582  A.wral 1642  E.wrex 1643   \ cdif 2040   (_ wss 2043  (/)c0 2276  |^|cint 2528  Ord word 2942  Oncon0 2943  suc csuc 2945  omcom 3126

This theorem is referenced by:  unblem2 4524  unblem3 4525

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127

Copyright terms: Public domain