Step Hyp Ref
Expression 1 elex 3118 . 2
2 limsuc 6684 . . . . . . . . . . . . . . . . . 18
3 2 biimpd 207 . . . . . . . . . . . . . . . . 17
4 sseq1 3524 . . . . . . . . . . . . . . . . . . . 20
5 4 rexbidv 2968 . . . . . . . . . . . . . . . . . . 19
6 5 rspcv 3206 . . . . . . . . . . . . . . . . . 18
7 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
8 sucssel 4975 . . . . . . . . . . . . . . . . . . . . 21
9 7 , 8 ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
10 9 reximi 2925 . . . . . . . . . . . . . . . . . . 19
11 eluni2 4253 . . . . . . . . . . . . . . . . . . 19
12 10 , 11 sylibr 212 . . . . . . . . . . . . . . . . . 18
13 6 , 12 syl6com 35 . . . . . . . . . . . . . . . . 17
14 3 , 13 syl9 71 . . . . . . . . . . . . . . . 16
15 14 ralrimdv 2873 . . . . . . . . . . . . . . 15
16 dfss3 3493 . . . . . . . . . . . . . . 15
17 15 , 16 syl6ibr 227 . . . . . . . . . . . . . 14
18 17 adantr 465 . . . . . . . . . . . . 13
19 uniss 4270 . . . . . . . . . . . . . . 15
20 limuni 4943 . . . . . . . . . . . . . . . 16
21 20 sseq2d 3531 . . . . . . . . . . . . . . 15
22 19 , 21 syl5ibr 221 . . . . . . . . . . . . . 14
23 22 imp 429 . . . . . . . . . . . . 13
24 18 , 23 jctird 544 . . . . . . . . . . . 12
25 eqss 3518 . . . . . . . . . . . 12
26 24 , 25 syl6ibr 227 . . . . . . . . . . 11
27 26 imdistanda 693 . . . . . . . . . 10
28 27 anim2d 565 . . . . . . . . 9
29 28 eximdv 1710 . . . . . . . 8
30 29 ss2abdv 3572 . . . . . . 7
31 intss 4307 . . . . . . 7
32 30 , 31 syl 16 . . . . . 6
33 32 adantl 466 . . . . 5
34 limelon 4946 . . . . . 6
35 cfval 8648 . . . . . 6
36 34 , 35 syl 16 . . . . 5
37 33 , 36 sseqtr4d 3540 . . . 4
38 cfub 8650 . . . . 5
39 eqimss 3555 . . . . . . . . . 10
40 39 anim2i 569 . . . . . . . . 9
41 40 anim2i 569 . . . . . . . 8
42 41 eximi 1656 . . . . . . 7
43 42 ss2abi 3571 . . . . . 6
44 intss 4307 . . . . . 6
45 43 , 44 ax-mp 5 . . . . 5
46 38 , 45 sstri 3512 . . . 4
47 37 , 46 jctil 537 . . 3
48 eqss 3518 . . 3
49 47 , 48 sylibr 212 . 2
50 1 , 49 sylan 471 1
