Step | Hyp | Ref
| Expression |
1 | | lmcnp.3 |
. . . . . . . 8
|
2 | | lmrcl 12985 |
. . . . . . . 8
|
3 | 1, 2 | syl 14 |
. . . . . . 7
|
4 | | toptopon2 12811 |
. . . . . . 7
TopOn |
5 | 3, 4 | sylib 121 |
. . . . . 6
TopOn |
6 | | lmcnp.k |
. . . . . . 7
|
7 | | toptopon2 12811 |
. . . . . . 7
TopOn |
8 | 6, 7 | sylib 121 |
. . . . . 6
TopOn |
9 | | lmcnp.4 |
. . . . . 6
|
10 | | cnpf2 13001 |
. . . . . 6
TopOn TopOn
|
11 | 5, 8, 9, 10 | syl3anc 1233 |
. . . . 5
|
12 | | nnuz 9522 |
. . . . . . . . . 10
|
13 | | 1zzd 9239 |
. . . . . . . . . 10
|
14 | 5, 12, 13 | lmbr2 13008 |
. . . . . . . . 9
|
15 | 1, 14 | mpbid 146 |
. . . . . . . 8
|
16 | 15 | simp1d 1004 |
. . . . . . 7
|
17 | | uniexg 4424 |
. . . . . . . . 9
|
18 | 3, 17 | syl 14 |
. . . . . . . 8
|
19 | | cnex 7898 |
. . . . . . . 8
|
20 | | elpm2g 6643 |
. . . . . . . 8
|
21 | 18, 19, 20 | sylancl 411 |
. . . . . . 7
|
22 | 16, 21 | mpbid 146 |
. . . . . 6
|
23 | 22 | simpld 111 |
. . . . 5
|
24 | | fco 5363 |
. . . . 5
|
25 | 11, 23, 24 | syl2anc 409 |
. . . 4
|
26 | 25 | fdmd 5354 |
. . . . 5
|
27 | 26 | feq2d 5335 |
. . . 4
|
28 | 25, 27 | mpbird 166 |
. . 3
|
29 | 22 | simprd 113 |
. . . 4
|
30 | 26, 29 | eqsstrd 3183 |
. . 3
|
31 | | uniexg 4424 |
. . . . 5
|
32 | 6, 31 | syl 14 |
. . . 4
|
33 | | elpm2g 6643 |
. . . 4
|
34 | 32, 19, 33 | sylancl 411 |
. . 3
|
35 | 28, 30, 34 | mpbir2and 939 |
. 2
|
36 | 15 | simp2d 1005 |
. . 3
|
37 | 11, 36 | ffvelrnd 5632 |
. 2
|
38 | 15 | simp3d 1006 |
. . . . . 6
|
39 | 38 | adantr 274 |
. . . . 5
|
40 | 5 | adantr 274 |
. . . . . 6
TopOn |
41 | 8 | adantr 274 |
. . . . . 6
TopOn |
42 | 36 | adantr 274 |
. . . . . 6
|
43 | 9 | adantr 274 |
. . . . . 6
|
44 | | simprl 526 |
. . . . . 6
|
45 | | simprr 527 |
. . . . . 6
|
46 | | icnpimaex 13005 |
. . . . . 6
TopOn
TopOn
|
47 | 40, 41, 42, 43, 44, 45, 46 | syl33anc 1248 |
. . . . 5
|
48 | | r19.29 2607 |
. . . . . . 7
|
49 | | pm3.45 592 |
. . . . . . . . 9
|
50 | 49 | imp 123 |
. . . . . . . 8
|
51 | 50 | reximi 2567 |
. . . . . . 7
|
52 | 48, 51 | syl 14 |
. . . . . 6
|
53 | 11 | ad3antrrr 489 |
. . . . . . . . . . . . . . . . . 18
|
54 | 53 | ffnd 5348 |
. . . . . . . . . . . . . . . . 17
|
55 | | simplrl 530 |
. . . . . . . . . . . . . . . . . 18
|
56 | | elssuni 3824 |
. . . . . . . . . . . . . . . . . 18
|
57 | 55, 56 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
58 | | fnfvima 5730 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | 3expia 1200 |
. . . . . . . . . . . . . . . . 17
|
60 | 54, 57, 59 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
|
61 | 23 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . 18
|
62 | | fvco3 5567 |
. . . . . . . . . . . . . . . . . 18
|
63 | 61, 62 | sylan 281 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | eleq1d 2239 |
. . . . . . . . . . . . . . . 16
|
65 | 60, 64 | sylibrd 168 |
. . . . . . . . . . . . . . 15
|
66 | | simplrr 531 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | sseld 3146 |
. . . . . . . . . . . . . . 15
|
68 | 65, 67 | syld 45 |
. . . . . . . . . . . . . 14
|
69 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
70 | 26 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
|
71 | 69, 70 | eleqtrrd 2250 |
. . . . . . . . . . . . . 14
|
72 | 68, 71 | jctild 314 |
. . . . . . . . . . . . 13
|
73 | 72 | expimpd 361 |
. . . . . . . . . . . 12
|
74 | 73 | ralimdv 2538 |
. . . . . . . . . . 11
|
75 | 74 | reximdv 2571 |
. . . . . . . . . 10
|
76 | 75 | expr 373 |
. . . . . . . . 9
|
77 | 76 | com23 78 |
. . . . . . . 8
|
78 | 77 | impd 252 |
. . . . . . 7
|
79 | 78 | rexlimdva 2587 |
. . . . . 6
|
80 | 52, 79 | syl5 32 |
. . . . 5
|
81 | 39, 47, 80 | mp2and 431 |
. . . 4
|
82 | 81 | expr 373 |
. . 3
|
83 | 82 | ralrimiva 2543 |
. 2
|
84 | 8, 12, 13 | lmbr2 13008 |
. 2
|
85 | 35, 37, 83, 84 | mpbir3and 1175 |
1
|