Step | Hyp | Ref
| Expression |
1 | | sseq1 3626 |
. . . . . 6
|
2 | 1 | anbi2d 740 |
. . . . 5
|
3 | | fveq2 6191 |
. . . . . 6
|
4 | 3 | eleq1d 2686 |
. . . . 5
|
5 | 2, 4 | imbi12d 334 |
. . . 4
|
6 | | sseq1 3626 |
. . . . . 6
|
7 | 6 | anbi2d 740 |
. . . . 5
|
8 | | fveq2 6191 |
. . . . . 6
|
9 | 8 | eleq1d 2686 |
. . . . 5
|
10 | 7, 9 | imbi12d 334 |
. . . 4
|
11 | | sseq1 3626 |
. . . . . 6
|
12 | 11 | anbi2d 740 |
. . . . 5
|
13 | | fveq2 6191 |
. . . . . 6
|
14 | 13 | eleq1d 2686 |
. . . . 5
|
15 | 12, 14 | imbi12d 334 |
. . . 4
|
16 | | sseq1 3626 |
. . . . . 6
|
17 | 16 | anbi2d 740 |
. . . . 5
|
18 | | fveq2 6191 |
. . . . . 6
|
19 | 18 | eleq1d 2686 |
. . . . 5
|
20 | 17, 19 | imbi12d 334 |
. . . 4
|
21 | | pclfincl.c |
. . . . . . 7
|
22 | 21 | pcl0N 35208 |
. . . . . 6
|
23 | | pclfincl.s |
. . . . . . 7
|
24 | 23 | 0psubclN 35229 |
. . . . . 6
|
25 | 22, 24 | eqeltrd 2701 |
. . . . 5
|
26 | 25 | adantr 481 |
. . . 4
|
27 | | anass 681 |
. . . . . . 7
|
28 | | vex 3203 |
. . . . . . . . . . 11
|
29 | 28 | snss 4316 |
. . . . . . . . . 10
|
30 | 29 | anbi2i 730 |
. . . . . . . . 9
|
31 | | unss 3787 |
. . . . . . . . 9
|
32 | 30, 31 | bitri 264 |
. . . . . . . 8
|
33 | 32 | anbi2i 730 |
. . . . . . 7
|
34 | 27, 33 | bitr2i 265 |
. . . . . 6
|
35 | | simpllr 799 |
. . . . . . . . . . . . . . 15
|
36 | 35 | uneq1d 3766 |
. . . . . . . . . . . . . 14
|
37 | | uncom 3757 |
. . . . . . . . . . . . . . 15
|
38 | | un0 3967 |
. . . . . . . . . . . . . . 15
|
39 | 37, 38 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
40 | 36, 39 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . 12
|
42 | | simplrl 800 |
. . . . . . . . . . . . 13
|
43 | | hlatl 34647 |
. . . . . . . . . . . . . . 15
|
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
|
45 | | simprr 796 |
. . . . . . . . . . . . . 14
|
46 | | pclfincl.a |
. . . . . . . . . . . . . . 15
|
47 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
48 | 46, 47 | snatpsubN 35036 |
. . . . . . . . . . . . . 14
|
49 | 44, 45, 48 | syl2anc 693 |
. . . . . . . . . . . . 13
|
50 | 47, 21 | pclidN 35182 |
. . . . . . . . . . . . 13
|
51 | 42, 49, 50 | syl2anc 693 |
. . . . . . . . . . . 12
|
52 | 41, 51 | eqtrd 2656 |
. . . . . . . . . . 11
|
53 | 46, 23 | atpsubclN 35231 |
. . . . . . . . . . . 12
|
54 | 42, 45, 53 | syl2anc 693 |
. . . . . . . . . . 11
|
55 | 52, 54 | eqeltrd 2701 |
. . . . . . . . . 10
|
56 | 55 | exp43 640 |
. . . . . . . . 9
|
57 | | simplrl 800 |
. . . . . . . . . . . . . 14
|
58 | 46, 21 | pclssidN 35181 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
60 | | unss1 3782 |
. . . . . . . . . . . . . . . 16
|
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
|
62 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
|
63 | 46, 23 | psubclssatN 35227 |
. . . . . . . . . . . . . . . . 17
|
64 | 57, 62, 63 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
65 | | snssi 4339 |
. . . . . . . . . . . . . . . . 17
|
66 | 65 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
|
67 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
68 | 46, 67 | paddunssN 35094 |
. . . . . . . . . . . . . . . 16
|
69 | 57, 64, 66, 68 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
70 | 61, 69 | sstrd 3613 |
. . . . . . . . . . . . . 14
|
71 | 46, 67 | paddssat 35100 |
. . . . . . . . . . . . . . 15
|
72 | 57, 64, 66, 71 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
73 | 46, 21 | pclssN 35180 |
. . . . . . . . . . . . . 14
|
74 | 57, 70, 72, 73 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
75 | | simprr 796 |
. . . . . . . . . . . . . . . 16
|
76 | 46, 67, 23 | paddatclN 35235 |
. . . . . . . . . . . . . . . 16
|
77 | 57, 62, 75, 76 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
78 | 47, 23 | psubclsubN 35226 |
. . . . . . . . . . . . . . 15
|
79 | 57, 77, 78 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
80 | 47, 21 | pclidN 35182 |
. . . . . . . . . . . . . 14
|
81 | 57, 79, 80 | syl2anc 693 |
. . . . . . . . . . . . 13
|
82 | 74, 81 | sseqtrd 3641 |
. . . . . . . . . . . 12
|
83 | | hllat 34650 |
. . . . . . . . . . . . . . . . . 18
|
84 | 57, 83 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
85 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
|
86 | 46, 21 | pcl0bN 35209 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | 86 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 87 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . 18
|
89 | 85, 88 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
90 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
91 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
92 | 90, 91, 46, 67 | elpaddat 35090 |
. . . . . . . . . . . . . . . . 17
|
93 | 84, 64, 75, 89, 92 | syl31anc 1329 |
. . . . . . . . . . . . . . . 16
|
94 | | simp1rl 1126 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | 94 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
|
98 | | simpl13 1138 |
. . . . . . . . . . . . . . . . . . . . 21
|
99 | | unss 3787 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
100 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
101 | 99, 100 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
102 | 101 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . 22
|
103 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 47, 21 | elpcliN 35179 |
. . . . . . . . . . . . . . . . . . . . . 22
|
105 | 96, 102, 97, 103, 104 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . 21
|
106 | 28 | snss 4316 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
107 | 106 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
108 | 107 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
109 | 99, 108 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . 22
|
110 | 109 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | 90, 91, 46, 47 | psubspi2N 35034 |
. . . . . . . . . . . . . . . . . . . . 21
|
113 | 96, 97, 98, 105, 110, 111, 112 | syl33anc 1341 |
. . . . . . . . . . . . . . . . . . . 20
|
114 | 113 | exp520 1288 |
. . . . . . . . . . . . . . . . . . 19
|
115 | 114 | rexlimdv 3030 |
. . . . . . . . . . . . . . . . . 18
|
116 | 115 | 3expia 1267 |
. . . . . . . . . . . . . . . . 17
|
117 | 116 | impd 447 |
. . . . . . . . . . . . . . . 16
|
118 | 93, 117 | sylbid 230 |
. . . . . . . . . . . . . . 15
|
119 | 118 | ralrimdv 2968 |
. . . . . . . . . . . . . 14
|
120 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
|
121 | 120, 75 | jca 554 |
. . . . . . . . . . . . . . . 16
|
122 | 121, 32 | sylib 208 |
. . . . . . . . . . . . . . 15
|
123 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
124 | 46, 47, 21, 123 | elpclN 35178 |
. . . . . . . . . . . . . . 15
|
125 | 57, 122, 124 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
126 | 119, 125 | sylibrd 249 |
. . . . . . . . . . . . 13
|
127 | 126 | ssrdv 3609 |
. . . . . . . . . . . 12
|
128 | 82, 127 | eqssd 3620 |
. . . . . . . . . . 11
|
129 | 128, 77 | eqeltrd 2701 |
. . . . . . . . . 10
|
130 | 129 | exp43 640 |
. . . . . . . . 9
|
131 | 56, 130 | pm2.61dane 2881 |
. . . . . . . 8
|
132 | 131 | a2d 29 |
. . . . . . 7
|
133 | 132 | imp4b 613 |
. . . . . 6
|
134 | 34, 133 | syl5bi 232 |
. . . . 5
|
135 | 134 | ex 450 |
. . . 4
|
136 | 5, 10, 15, 20, 26, 135 | findcard2 8200 |
. . 3
|
137 | 136 | 3impib 1262 |
. 2
|
138 | 137 | 3coml 1272 |
1
|