Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. . . . 5
|
2 | | sucexb 7009 |
. . . . 5
|
3 | 1, 2 | sylibr 224 |
. . . 4
|
4 | | sssucid 5802 |
. . . . 5
|
5 | | elpwg 4166 |
. . . . 5
|
6 | 4, 5 | mpbiri 248 |
. . . 4
|
7 | | limsucncmpi.1 |
. . . . . . 7
|
8 | | limuni 5785 |
. . . . . . 7
|
9 | 7, 8 | ax-mp 5 |
. . . . . 6
|
10 | | elin 3796 |
. . . . . . . . . 10
|
11 | | elpwi 4168 |
. . . . . . . . . . 11
|
12 | 11 | anim1i 592 |
. . . . . . . . . 10
|
13 | 10, 12 | sylbi 207 |
. . . . . . . . 9
|
14 | | nlim0 5783 |
. . . . . . . . . . . . . . . 16
|
15 | 7, 14 | 2th 254 |
. . . . . . . . . . . . . . 15
|
16 | | xor3 372 |
. . . . . . . . . . . . . . 15
|
17 | 15, 16 | mpbir 221 |
. . . . . . . . . . . . . 14
|
18 | | limeq 5735 |
. . . . . . . . . . . . . . 15
|
19 | 18 | necon3bi 2820 |
. . . . . . . . . . . . . 14
|
20 | 17, 19 | ax-mp 5 |
. . . . . . . . . . . . 13
|
21 | | uni0 4465 |
. . . . . . . . . . . . 13
|
22 | 20, 21 | neeqtrri 2867 |
. . . . . . . . . . . 12
|
23 | | unieq 4444 |
. . . . . . . . . . . . 13
|
24 | 23 | neeq2d 2854 |
. . . . . . . . . . . 12
|
25 | 22, 24 | mpbiri 248 |
. . . . . . . . . . 11
|
26 | 25 | a1i 11 |
. . . . . . . . . 10
|
27 | | limord 5784 |
. . . . . . . . . . . . . 14
|
28 | | ordsson 6989 |
. . . . . . . . . . . . . 14
|
29 | 7, 27, 28 | mp2b 10 |
. . . . . . . . . . . . 13
|
30 | | sstr2 3610 |
. . . . . . . . . . . . 13
|
31 | 29, 30 | mpi 20 |
. . . . . . . . . . . 12
|
32 | | ordunifi 8210 |
. . . . . . . . . . . . 13
|
33 | 32 | 3expia 1267 |
. . . . . . . . . . . 12
|
34 | 31, 33 | sylan 488 |
. . . . . . . . . . 11
|
35 | | ssel 3597 |
. . . . . . . . . . . . 13
|
36 | 7, 27 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
37 | | nordeq 5742 |
. . . . . . . . . . . . . 14
|
38 | 36, 37 | mpan 706 |
. . . . . . . . . . . . 13
|
39 | 35, 38 | syl6 35 |
. . . . . . . . . . . 12
|
40 | 39 | adantr 481 |
. . . . . . . . . . 11
|
41 | 34, 40 | syld 47 |
. . . . . . . . . 10
|
42 | 26, 41 | pm2.61dne 2880 |
. . . . . . . . 9
|
43 | 13, 42 | syl 17 |
. . . . . . . 8
|
44 | 43 | neneqd 2799 |
. . . . . . 7
|
45 | 44 | nrex 3000 |
. . . . . 6
|
46 | | unieq 4444 |
. . . . . . . . 9
|
47 | 46 | eqeq2d 2632 |
. . . . . . . 8
|
48 | | pweq 4161 |
. . . . . . . . . . 11
|
49 | 48 | ineq1d 3813 |
. . . . . . . . . 10
|
50 | 49 | rexeqdv 3145 |
. . . . . . . . 9
|
51 | 50 | notbid 308 |
. . . . . . . 8
|
52 | 47, 51 | anbi12d 747 |
. . . . . . 7
|
53 | 52 | rspcev 3309 |
. . . . . 6
|
54 | 9, 45, 53 | mpanr12 721 |
. . . . 5
|
55 | | rexanali 2998 |
. . . . 5
|
56 | 54, 55 | sylib 208 |
. . . 4
|
57 | 3, 6, 56 | 3syl 18 |
. . 3
|
58 | | imnan 438 |
. . 3
|
59 | 57, 58 | mpbi 220 |
. 2
|
60 | | ordunisuc 7032 |
. . . . 5
|
61 | 7, 27, 60 | mp2b 10 |
. . . 4
|
62 | 61 | eqcomi 2631 |
. . 3
|
63 | 62 | iscmp 21191 |
. 2
|
64 | 59, 63 | mtbir 313 |
1
|