Proof of Theorem marypha1lem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | xpeq1 4702 |
. . . . 5
         |
| 2 | 1 | pweqd 3631 |
. . . 4
 |
| 3 | | pweq 3629 |
. . . . . 6
|
| 4 | 3 | raleqdv 2743 |
. . . . 5
 
    
|
| 5 | | f1eq2 5398 |
. . . . . 6
    |
| 6 | 5 | rexbidv 2565 |
. . . . 5
|
| 7 | 4, 6 | imbi12d 313 |
. . . 4
|
| 8 | 2, 7 | raleqbidv 2749 |
. . 3
|
| 9 | 8 | imbi2d 309 |
. 2
|
| 10 | | xpeq1 4702 |
. . . . 5
 |
| 11 | 10 | pweqd 3631 |
. . . 4
|
| 12 | | pweq 3629 |
. . . . . 6
|
| 13 | 12 | raleqdv 2743 |
. . . . 5
|
| 14 | | f1eq2 5398 |
. . . . . 6
|
| 15 | 14 | rexbidv 2565 |
. . . . 5
|
| 16 | 13, 15 | imbi12d 313 |
. . . 4
|
| 17 | 11, 16 | raleqbidv 2749 |
. . 3
|
| 18 | 17 | imbi2d 309 |
. 2
|
| 19 | | bi2.04 352 |
. . . . 5
 |
| 20 | 19 | albii 1558 |
. . . 4
|
| 21 | | 19.21v 1842 |
. . . 4
|
| 22 | 20, 21 | bitri 242 |
. . 3
|
| 23 | | 0elpw 4179 |
. . . . . . . . . . . . 13
  |
| 24 | | f10 5472 |
. . . . . . . . . . . . 13
|
| 25 | | f1eq1 5397 |
. . . . . . . . . . . . . 14
|
| 26 | 25 | rspcev 2885 |
. . . . . . . . . . . . 13
![/\](wedge.gif "/\") |
| 27 | 23, 24, 26 | mp2an 656 |
. . . . . . . . . . . 12
|
| 28 | | f1eq2 5398 |
. . . . . . . . . . . . 13
|
| 29 | 28 | rexbidv 2565 |
. . . . . . . . . . . 12
|
| 30 | 27, 29 | mpbiri 226 |
. . . . . . . . . . 11
|
| 31 | 30 | a1i 12 |
. . . . . . . . . 10
  |
| 32 | | n0 3465 |
. . . . . . . . . . 11
 |
| 33 | | snelpwi 4219 |
. . . . . . . . . . . . . . . . . . 19
  |
| 34 | | id 21 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 35 | | imaeq2 5007 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 36 | 34, 35 | breq12d 4037 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 37 | 36 | rspcva 2883 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 38 | | vex 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 39 | 38 | snnz 3745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 40 | | snex 4215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 41 | 40 | 0sdom 6987 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 42 | 39, 41 | mpbir 202 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 43 | | sdomdomtr 6989 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 44 | 42, 43 | mpan 654 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 45 | | vex 2792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 46 | | imaexg 5025 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 47 | 45, 46 | ax-mp 10 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 48 | 47 | 0sdom 6987 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 49 | 44, 48 | sylib 190 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 50 | 37, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
| 51 | 50 | expcom 426 |
. . . . . . . . . . . . . . . . . . 19
|
| 52 | 33, 51 | syl5 30 |
. . . . . . . . . . . . . . . . . 18
|
| 53 | 52 | adantl 454 |
. . . . . . . . . . . . . . . . 17
|
| 54 | 53 | ad2antlr 710 |
. . . . . . . . . . . . . . . 16
|
| 55 | 54 | impr 605 |
. . . . . . . . . . . . . . 15
|
| 56 | | n0 3465 |
. . . . . . . . . . . . . . 15
 |
| 57 | 55, 56 | sylib 190 |
. . . . . . . . . . . . . 14
|
| 58 | | imaexg 5025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 59 | | difexg 4163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![\](setminus.gif "\")
|
| 60 | 45, 58, 59 | mp2b 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 61 | 60 | 0dom 6986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 62 | | breq1 4027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 63 | 61, 62 | mpbiri 226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 64 | 63 | a1i 12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 65 | | simpll 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 66 | | elpwi 3634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
| 67 | 66 | ad2antrl 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 68 | | disjsn 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
|
| 69 | | disj4 3504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 70 | 68, 69 | bitr3i 244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 71 | 70 | con4bii 290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 72 | 71 | biimpi 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 73 | 72 | ad2antlr 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 74 | | sspsstr 3282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 75 | 67, 73, 74 | syl2anc 645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 76 | | simprr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 77 | 75, 76 | jca 520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 78 | | psseq1 3264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 79 | | neeq1 2455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 80 | 78, 79 | anbi12d 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 81 | | id 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 82 | | imaeq2 5007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 83 | 81, 82 | breq12d 4037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 84 | 80, 83 | imbi12d 313 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 85 | 84 | spv 2018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 86 | 65, 77, 85 | sylc 58 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 87 | | domdifsn 6940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 89 | 88 | expr 601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 90 | 64, 89 | pm2.61dne 2524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 91 | 90 | adantlrr 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 92 | 91 | adantll 697 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 93 | | df-ss 3167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 94 | 66, 93 | sylib 190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 95 | 94 | imaeq2d 5011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 96 | 95 | ineq1d 3370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 97 | 96 | adantl 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 98 | | indif2 3413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 99 | | imassrn 5024 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
| 100 | | elpwi 3634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 101 | | rnss 4906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 102 | | rnxpss 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 103 | 101, 102 | syl6ss 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 104 | 100, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 105 | 99, 104 | syl5ss 3191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 106 | | df-ss 3167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 107 | 105, 106 | sylib 190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 108 | 107 | difeq1d 3294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 109 | 108 | ad2antrl 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 110 | 98, 109 | syl5eq 2328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 111 | 110 | ad2antrr 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 112 | 97, 111 | eqtrd 2316 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 113 | 92, 112 | breqtrrd 4050 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 114 | 113 | ralrimiva 2627 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 115 | | id 21 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 116 | | imainrect 5118 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 117 | | imaeq2 5007 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 118 | 116, 117 | syl5eqr 2330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 119 | 115, 118 | breq12d 4037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 120 | 119 | cbvralv 2765 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 121 | 114, 120 | sylib 190 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 122 | 121 | adantllr 702 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 123 | | inss2 3391 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 124 | | difss 3304 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 125 | | xpss2 4795 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 126 | 124, 125 | ax-mp 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 127 | 123, 126 | sstri 3189 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 128 | 45 | inex1 4156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 129 | 128 | elpw 3632 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 130 | 127, 129 | mpbir 202 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 131 | | simpllr 738 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 132 | 72 | adantr 453 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 133 | 132 | ad2antll 712 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 134 | | vex 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 135 | | difexg 4163 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 136 | 134, 135 | ax-mp 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 137 | | psseq1 3264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 138 | | xpeq1 4702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 139 | 138 | pweqd 3631 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 140 | | pweq 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 141 | 140 | raleqdv 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 142 | | f1eq2 5398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 143 | 142 | rexbidv 2565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 144 | 141, 143 | imbi12d 313 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 145 | 139, 144 | raleqbidv 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 146 | 137, 145 | imbi12d 313 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 147 | 136, 146 | spcv 2875 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 148 | 131, 133,
147 | sylc 58 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 149 | | imaeq1 5006 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 150 | 149 | breq2d 4036 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 151 | 150 | ralbidv 2564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 152 | | pweq 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 153 | 152 | rexeqdv 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 154 | 151, 153 | imbi12d 313 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 155 | 154 | rspcva 2883 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 156 | 130, 148,
155 | sylancr 647 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 157 | 122, 156 | mpd 16 |
. . . . . . . . . . . . . . . . . . . 20
|
| 158 | | f1eq1 5397 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 159 | 158 | cbvrexv 2766 |
. . . . . . . . . . . . . . . . . . . 20
|
| 160 | 157, 159 | sylib 190 |
. . . . . . . . . . . . . . . . . . 19
|
| 161 | | vex 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 162 | 38, 161 | elimasn 5037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
| 163 | 162 | biimpi 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 164 | 163 | snssd 3761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 165 | 164 | ad2antlr 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 166 | | elpwi 3634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 167 | | inss1 3390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 168 | 166, 167 | syl6ss 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 169 | 168 | adantl 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 170 | 165, 169 | unssd 3352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 171 | 45 | elpw2 4169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 172 | 170, 171 | sylibr 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 173 | 172 | ad2ant2lr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 174 | 38, 161 | f1osn 5478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
| 175 | 174 | a1i 12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 176 | | f1f1orn 5448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 177 | 176 | adantl 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 178 | | disjdif 3527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 179 | 178 | a1i 12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 180 | | incom 3362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 181 | 166, 123 | syl6ss 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 182 | | rnss 4906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 183 | | rnxpss 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 184 | 182, 183 | syl6ss 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 186 | | incom 3362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 187 | | disjdif 3527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 188 | 186, 187 | eqtri 2304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 189 | | ssdisj 3505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 190 | 185, 188,
189 | sylancl 646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 191 | 180, 190 | syl5eq 2328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 192 | 191 | adantr 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 193 | | f1oun 5457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 194 | 175, 177,
179, 192, 193 | syl22anc 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 195 | 194 | adantl 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 196 | | snssi 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 197 | 196 | ad2antrl 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 198 | | undif 3535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 199 | 197, 198 | sylib 190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 200 | | f1oeq2 5429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 202 | 201 | adantr 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 203 | 195, 202 | mpbid 203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 204 | | f1of1 5436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 205 | | ssv 3199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 206 | | f1ss 5407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 207 | 204, 205,
206 | sylancl 646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 208 | 203, 207 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 209 | | f1eq1 5397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 210 | 209 | rspcev 2885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 211 | 173, 208,
210 | syl2anc 645 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 212 | 211 | exp32 591 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 213 | 212 | rexlimdv 2667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 214 | 213 | ex 425 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 215 | 214 | adantr 453 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 216 | 215 | ad2antlr 710 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 217 | 216 | impr 605 |
. . . . . . . . . . . . . . . . . . . 20
|
| 218 | 217 | adantllr 702 |
. . . . . . . . . . . . . . . . . . 19
|
| 219 | 160, 218 | mpd 16 |
. . . . . . . . . . . . . . . . . 18
|
| 220 | 219 | expr 601 |
. . . . . . . . . . . . . . . . 17
|
| 221 | 220 | exp3a 427 |
. . . . . . . . . . . . . . . 16
|
| 222 | 221 | impr 605 |
. . . . . . . . . . . . . . 15
|
| 223 | 222 | exlimdv 1668 |
. . . . . . . . . . . . . 14
|
| 224 | 57, 223 | mpd 16 |
. . . . . . . . . . . . 13
|
| 225 | 224 | expr 601 |
. . . . . . . . . . . 12
|
| 226 | 225 | exlimdv 1668 |
. . . . . . . . . . 11
|
| 227 | 32, 226 | syl5bi 210 |
. . . . . . . . . 10
|
| 228 | 31, 227 | pm2.61dne 2524 |
. . . . . . . . 9
|
| 229 | | exanali 1577 |
. . . . . . . . . 10
|
| 230 | | simprll 741 |
. . . . . . . . . . . . . . . . . . . 20
|
| 231 | | pssss 3272 |
. . . . . . . . . . . . . . . . . . . 20
|
| 232 | 230, 231 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 233 | | sspwb 4222 |
. . . . . . . . . . . . . . . . . . 19
|
| 234 | 232, 233 | sylib 190 |
. . . . . . . . . . . . . . . . . 18
|
| 235 | | simplrr 740 |
. . . . . . . . . . . . . . . . . 18
|
| 236 | | ssralv 3238 |
. . . . . . . . . . . . . . . . . 18
|
| 237 | 234, 235,
236 | sylc 58 |
. . . . . . . . . . . . . . . . 17
|
| 238 | | elpwi 3634 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 239 | | resima2 4987 |
. . . . . . . . . . . . . . . . . . . . 21
 |
| 240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
| 241 | 240 | eqcomd 2289 |
. . . . . . . . . . . . . . . . . . 19
|
| 242 | 241 | breq2d 4036 |
. . . . . . . . . . . . . . . . . 18
|
| 243 | 242 | ralbiia 2576 |
. . . . . . . . . . . . . . . . 17
|
| 244 | 237, 243 | sylib 190 |
. . . . . . . . . . . . . . . 16
|
| 245 | | simplrl 739 |
. . . . . . . . . . . . . . . . . 18
|
| 246 | | ssres 4980 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 247 | | df-res 4700 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 248 | | inxp 4817 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 249 | | inss2 3391 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 250 | | inss1 3390 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 251 | | xpss12 4791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 252 | 249, 250,
251 | mp2an 656 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 253 | 248, 252 | eqsstri 3209 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 254 | 247, 253 | eqsstri 3209 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 255 | 246, 254 | syl6ss 3192 |
. . . . . . . . . . . . . . . . . . . 20
|
| 256 | 100, 255 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 257 | 45 | resex 4994 |
. . . . . . . . . . . . . . . . . . . 20
|
| 258 | 257 | elpw 3632 |
. . . . . . . . . . . . . . . . . . 19
|
| 259 | 256, 258 | sylibr 205 |
. . . . . . . . . . . . . . . . . 18
|
| 260 | 245, 259 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
| 261 | | simpllr 738 |
. . . . . . . . . . . . . . . . . 18
|
| 262 | | psseq1 3264 |
. . . . . . . . . . . . . . . . . . . 20
|
| 263 | | xpeq1 4702 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 264 | 263 | pweqd 3631 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 265 | | pweq 3629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 266 | 265 | raleqdv 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 267 | | f1eq2 5398 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 268 | 267 | rexbidv 2565 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 269 | 266, 268 | imbi12d 313 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 270 | 264, 269 | raleqbidv 2749 |
. . . . . . . . . . . . . . . . . . . 20
|
| 271 | 262, 270 | imbi12d 313 |
. . . . . . . . . . . . . . . . . . 19
|
| 272 | 271 | spv 2018 |
. . . . . . . . . . . . . . . . . 18
|
| 273 | 261, 230,
272 | sylc 58 |
. . . . . . . . . . . . . . . . 17
|
| 274 | | imaeq1 5006 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 275 | 274 | breq2d 4036 |
. . . . . . . . . . . . . . . . . . . 20
|
| 276 | 275 | ralbidv 2564 |
. . . . . . . . . . . . . . . . . . 19
|
| 277 | | pweq 3629 |
. . . . . . . . . . . . . . . . . . . 20
|
| 278 | 277 | rexeqdv 2744 |
. . . . . . . . . . . . . . . . . . 19
|
| 279 | 276, 278 | imbi12d 313 |
. . . . . . . . . . . . . . . . . 18
|
| 280 | 279 | rspcva 2883 |
. . . . . . . . . . . . . . . . 17
|
| 281 | 260, 273,
280 | syl2anc 645 |
. . . . . . . . . . . . . . . 16
|
| 282 | 244, 281 | mpd 16 |
. . . . . . . . . . . . . . 15
|
| 283 | | f1eq1 5397 |
. . . . . . . . . . . . . . . 16
|
| 284 | 283 | cbvrexv 2766 |
. . . . . . . . . . . . . . 15
|
| 285 | 282, 284 | sylib 190 |
. . . . . . . . . . . . . 14
|
| 286 | 231 | ad2antrr 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 287 | 286 | ad2antlr 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 288 | | elpwi 3634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 289 | | difss 3304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 290 | 288, 289 | syl6ss 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 291 | 290 | adantl 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 292 | 287, 291 | unssd 3352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 293 | 134 | elpw2 4169 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 294 | 292, 293 | sylibr 205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 295 | | simprr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 296 | 295 | ad2antrr 709 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 297 | | id 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 298 | | imaeq2 5007 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
