Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . 7
|
2 | | cnrefiisplem.a |
. . . . . . . . 9
|
3 | | cnrefiisplem.n |
. . . . . . . . 9
|
4 | 2, 3 | absimnre 39707 |
. . . . . . . 8
|
5 | 4 | adantr 481 |
. . . . . . 7
|
6 | 1, 5 | eqeltrd 2701 |
. . . . . 6
|
7 | 6 | adantlr 751 |
. . . . 5
|
8 | | simpll 790 |
. . . . . 6
|
9 | | cnrefiisplem.d |
. . . . . . . . . . . 12
|
10 | 9 | eleq2i 2693 |
. . . . . . . . . . 11
|
11 | 10 | biimpi 206 |
. . . . . . . . . 10
|
12 | | nelsn 4212 |
. . . . . . . . . 10
|
13 | | elunnel1 3754 |
. . . . . . . . . 10
|
14 | 11, 12, 13 | syl2an 494 |
. . . . . . . . 9
|
15 | | eliun 4524 |
. . . . . . . . 9
|
16 | 14, 15 | sylib 208 |
. . . . . . . 8
|
17 | | velsn 4193 |
. . . . . . . . 9
|
18 | 17 | rexbii 3041 |
. . . . . . . 8
|
19 | 16, 18 | sylib 208 |
. . . . . . 7
|
20 | 19 | adantll 750 |
. . . . . 6
|
21 | | simpr 477 |
. . . . . . . 8
|
22 | | eldifi 3732 |
. . . . . . . . . . . 12
|
23 | 22 | elin2d 3803 |
. . . . . . . . . . 11
|
24 | 23 | ad2antlr 763 |
. . . . . . . . . 10
|
25 | 2 | ad2antrr 762 |
. . . . . . . . . 10
|
26 | 24, 25 | subcld 10392 |
. . . . . . . . 9
|
27 | | eldifsni 4320 |
. . . . . . . . . . 11
|
28 | 27 | ad2antlr 763 |
. . . . . . . . . 10
|
29 | 24, 25, 28 | subne0d 10401 |
. . . . . . . . 9
|
30 | 26, 29 | absrpcld 14187 |
. . . . . . . 8
|
31 | 21, 30 | eqeltrd 2701 |
. . . . . . 7
|
32 | 31 | rexlimdva2 39339 |
. . . . . 6
|
33 | 8, 20, 32 | sylc 65 |
. . . . 5
|
34 | 7, 33 | pm2.61dane 2881 |
. . . 4
|
35 | 34 | ssd 39252 |
. . 3
|
36 | | cnrefiisplem.x |
. . . 4
inf |
37 | | xrltso 11974 |
. . . . . 6
|
38 | 37 | a1i 11 |
. . . . 5
|
39 | | snfi 8038 |
. . . . . . . 8
|
40 | 39 | a1i 11 |
. . . . . . 7
|
41 | | cnrefiisplem.b |
. . . . . . . . 9
|
42 | | inss1 3833 |
. . . . . . . . . . 11
|
43 | 42 | a1i 11 |
. . . . . . . . . 10
|
44 | 43 | ssdifssd 3748 |
. . . . . . . . 9
|
45 | 41, 44 | ssfid 8183 |
. . . . . . . 8
|
46 | | snfi 8038 |
. . . . . . . . 9
|
47 | 46 | rgenw 2924 |
. . . . . . . 8
|
48 | | iunfi 8254 |
. . . . . . . 8
|
49 | 45, 47, 48 | sylancl 694 |
. . . . . . 7
|
50 | 40, 49 | unfid 39345 |
. . . . . 6
|
51 | 9, 50 | syl5eqel 2705 |
. . . . 5
|
52 | | fvex 6201 |
. . . . . . . . . 10
|
53 | 52 | snid 4208 |
. . . . . . . . 9
|
54 | | elun1 3780 |
. . . . . . . . 9
|
55 | 53, 54 | ax-mp 5 |
. . . . . . . 8
|
56 | 55, 9 | eleqtrri 2700 |
. . . . . . 7
|
57 | 56 | a1i 11 |
. . . . . 6
|
58 | 57 | ne0d 39308 |
. . . . 5
|
59 | | rpssxr 39711 |
. . . . . 6
|
60 | 35, 59 | syl6ss 3615 |
. . . . 5
|
61 | | fiinfcl 8407 |
. . . . 5
inf |
62 | 38, 51, 58, 60, 61 | syl13anc 1328 |
. . . 4
inf |
63 | 36, 62 | syl5eqel 2705 |
. . 3
|
64 | 35, 63 | sseldd 3604 |
. 2
|
65 | 35, 62 | sseldd 3604 |
. . . . . . . . . 10
inf |
66 | 65 | rpred 11872 |
. . . . . . . . 9
inf |
67 | 66 | adantr 481 |
. . . . . . . 8
inf |
68 | 2 | imcld 13935 |
. . . . . . . . . . 11
|
69 | 68 | recnd 10068 |
. . . . . . . . . 10
|
70 | 69 | adantr 481 |
. . . . . . . . 9
|
71 | 70 | abscld 14175 |
. . . . . . . 8
|
72 | | recn 10026 |
. . . . . . . . . . 11
|
73 | 72 | adantl 482 |
. . . . . . . . . 10
|
74 | 2 | adantr 481 |
. . . . . . . . . 10
|
75 | 73, 74 | subcld 10392 |
. . . . . . . . 9
|
76 | 75 | abscld 14175 |
. . . . . . . 8
|
77 | 60 | adantr 481 |
. . . . . . . . 9
|
78 | | infxrlb 12164 |
. . . . . . . . 9
inf |
79 | 77, 56, 78 | sylancl 694 |
. . . . . . . 8
inf |
80 | | simpr 477 |
. . . . . . . . 9
|
81 | 74, 80 | absimlere 39710 |
. . . . . . . 8
|
82 | 67, 71, 76, 79, 81 | letrd 10194 |
. . . . . . 7
inf |
83 | 36, 82 | syl5eqbr 4688 |
. . . . . 6
|
84 | 83 | ad4ant14 1293 |
. . . . 5
|
85 | | cnrefiisplem.c |
. . . . . . . . 9
|
86 | 85 | eleq2i 2693 |
. . . . . . . 8
|
87 | | elunnel1 3754 |
. . . . . . . 8
|
88 | 86, 87 | sylanb 489 |
. . . . . . 7
|
89 | 88 | ad4ant24 1298 |
. . . . . 6
|
90 | 60 | ad2antrr 762 |
. . . . . . . . 9
|
91 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
92 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
93 | 91, 92 | elind 3798 |
. . . . . . . . . . . . . . 15
|
94 | | nelsn 4212 |
. . . . . . . . . . . . . . . 16
|
95 | 94 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
96 | 93, 95 | eldifd 3585 |
. . . . . . . . . . . . . 14
|
97 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
98 | 97 | snid 4208 |
. . . . . . . . . . . . . 14
|
99 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
100 | 99 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
101 | 100 | sneqd 4189 |
. . . . . . . . . . . . . . 15
|
102 | 101 | eliuni 4526 |
. . . . . . . . . . . . . 14
|
103 | 96, 98, 102 | sylancl 694 |
. . . . . . . . . . . . 13
|
104 | 101 | cbviunv 4559 |
. . . . . . . . . . . . 13
|
105 | 103, 104 | syl6eleq 2711 |
. . . . . . . . . . . 12
|
106 | | elun2 3781 |
. . . . . . . . . . . 12
|
107 | 105, 106 | syl 17 |
. . . . . . . . . . 11
|
108 | 107, 9 | syl6eleqr 2712 |
. . . . . . . . . 10
|
109 | 108 | adantll 750 |
. . . . . . . . 9
|
110 | | infxrlb 12164 |
. . . . . . . . 9
inf |
111 | 90, 109, 110 | syl2anc 693 |
. . . . . . . 8
inf |
112 | 36, 111 | syl5eqbr 4688 |
. . . . . . 7
|
113 | 112 | adantllr 755 |
. . . . . 6
|
114 | 89, 113 | syldan 487 |
. . . . 5
|
115 | 84, 114 | pm2.61dan 832 |
. . . 4
|
116 | 115 | ex 450 |
. . 3
|
117 | 116 | ralrimiva 2966 |
. 2
|
118 | | breq1 4656 |
. . . . 5
|
119 | 118 | imbi2d 330 |
. . . 4
|
120 | 119 | ralbidv 2986 |
. . 3
|
121 | 120 | rspcev 3309 |
. 2
|
122 | 64, 117, 121 | syl2anc 693 |
1
|