Step | Hyp | Ref
| Expression |
1 | | simplll 798 |
. . . . . . . . . . . 12
FinII
FinII |
2 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . 19
|
3 | | sstr 3611 |
. . . . . . . . . . . . . . . . . . 19
|
4 | 2, 3 | mpan 706 |
. . . . . . . . . . . . . . . . . 18
|
5 | | elpw2g 4827 |
. . . . . . . . . . . . . . . . . . 19
FinII
|
6 | 5 | biimpar 502 |
. . . . . . . . . . . . . . . . . 18
FinII
|
7 | 4, 6 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
FinII
|
8 | 7 | ralrimivw 2967 |
. . . . . . . . . . . . . . . 16
FinII
|
9 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
10 | 9 | rabex 4813 |
. . . . . . . . . . . . . . . . . 18
|
11 | 10 | rgenw 2924 |
. . . . . . . . . . . . . . . . 17
|
12 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
13 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
|
14 | 12, 13 | ralrnmpt 6368 |
. . . . . . . . . . . . . . . . 17
|
15 | 11, 14 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
16 | 8, 15 | sylibr 224 |
. . . . . . . . . . . . . . 15
FinII
|
17 | | dfss3 3592 |
. . . . . . . . . . . . . . 15
|
18 | 16, 17 | sylibr 224 |
. . . . . . . . . . . . . 14
FinII
|
19 | 18 | adantlr 751 |
. . . . . . . . . . . . 13
FinII
|
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
FinII
|
21 | 10, 12 | dmmpti 6023 |
. . . . . . . . . . . . . . 15
|
22 | 21 | neeq1i 2858 |
. . . . . . . . . . . . . 14
|
23 | | dm0rn0 5342 |
. . . . . . . . . . . . . . 15
|
24 | 23 | necon3bii 2846 |
. . . . . . . . . . . . . 14
|
25 | 22, 24 | sylbb1 227 |
. . . . . . . . . . . . 13
|
26 | 25 | adantl 482 |
. . . . . . . . . . . 12
FinII
|
27 | | soss 5053 |
. . . . . . . . . . . . . . . 16
|
28 | 27 | impcom 446 |
. . . . . . . . . . . . . . 15
|
29 | | porpss 6941 |
. . . . . . . . . . . . . . . . 17
[] |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
[] |
31 | | solin 5058 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
32 | | fin2solem 33395 |
. . . . . . . . . . . . . . . . . . . . . . . 24
[] |
33 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
34 | 33 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
36 | | fin2solem 33395 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
[] |
37 | 36 | ancom2s 844 |
. . . . . . . . . . . . . . . . . . . . . . . 24
[] |
38 | 32, 35, 37 | 3orim123d 1407 |
. . . . . . . . . . . . . . . . . . . . . . 23
[] []
|
39 | 31, 38 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
[] []
|
40 | 39 | ralrimivva 2971 |
. . . . . . . . . . . . . . . . . . . . 21
[] []
|
41 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
[]
[]
|
42 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
43 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
[]
[] |
44 | 41, 42, 43 | 3orbi123d 1398 |
. . . . . . . . . . . . . . . . . . . . . . . 24
[]
[]
[] []
|
45 | 44 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . 23
[]
[]
[] []
|
46 | 12, 45 | ralrnmpt 6368 |
. . . . . . . . . . . . . . . . . . . . . 22
[] []
[] []
|
47 | 11, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
[]
[]
[] []
|
48 | 40, 47 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
[] [] |
49 | 48 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . 19
[] [] |
50 | 9 | rabex 4813 |
. . . . . . . . . . . . . . . . . . . . 21
|
51 | 50 | rgenw 2924 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | 34 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . 22
[]
[]
|
54 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . 22
|
55 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . 22
[]
[] |
56 | 53, 54, 55 | 3orbi123d 1398 |
. . . . . . . . . . . . . . . . . . . . 21
[]
[] []
[] |
57 | 52, 56 | ralrnmpt 6368 |
. . . . . . . . . . . . . . . . . . . 20
[]
[]
[]
[] |
58 | 51, 57 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
[]
[]
[]
[] |
59 | 49, 58 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
[]
[] |
60 | 59 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . 17
[]
[] |
61 | 60 | anasss 679 |
. . . . . . . . . . . . . . . 16
[] [] |
62 | 30, 61 | issod 5065 |
. . . . . . . . . . . . . . 15
[] |
63 | 28, 62 | syl 17 |
. . . . . . . . . . . . . 14
[]
|
64 | 63 | adantll 750 |
. . . . . . . . . . . . 13
FinII [] |
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
FinII
[] |
66 | | fin2i2 9140 |
. . . . . . . . . . . 12
FinII
[] |
67 | 1, 20, 26, 65, 66 | syl22anc 1327 |
. . . . . . . . . . 11
FinII
|
68 | 52, 50 | elrnmpti 5376 |
. . . . . . . . . . 11
|
69 | 67, 68 | sylib 208 |
. . . . . . . . . 10
FinII
|
70 | | ssel2 3598 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | | sonr 5056 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 70, 71 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 72 | anassrs 680 |
. . . . . . . . . . . . . . . . . 18
|
74 | 73 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
76 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
|
77 | 76 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 77 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . 19
|
79 | 78 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
80 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
81 | 80 | elint2 4482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
82 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
83 | 12, 82 | ralrnmpt 6368 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
84 | 11, 83 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
85 | 81, 84 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
87 | 86 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
88 | 87 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
89 | 88 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
90 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
91 | 90 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
92 | 91 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | 89, 92 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
|
94 | 93 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 85, 94 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 96 | imbi1d 331 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 95, 97 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 98 | imp 445 |
. . . . . . . . . . . . . . . . . 18
|
100 | 79, 99 | syld 47 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | adantlll 754 |
. . . . . . . . . . . . . . . 16
|
102 | 75, 101 | mtod 189 |
. . . . . . . . . . . . . . 15
|
103 | 102 | ex 450 |
. . . . . . . . . . . . . 14
|
104 | 103 | ralrimdva 2969 |
. . . . . . . . . . . . 13
|
105 | 104 | reximdva 3017 |
. . . . . . . . . . . 12
|
106 | 105 | adantll 750 |
. . . . . . . . . . 11
FinII
|
107 | 106 | adantr 481 |
. . . . . . . . . 10
FinII
|
108 | 69, 107 | mpd 15 |
. . . . . . . . 9
FinII
|
109 | 108 | expl 648 |
. . . . . . . 8
FinII
|
110 | 109 | alrimiv 1855 |
. . . . . . 7
FinII
|
111 | | df-fr 5073 |
. . . . . . 7
|
112 | 110, 111 | sylibr 224 |
. . . . . 6
FinII
|
113 | | simpr 477 |
. . . . . 6
FinII
|
114 | | df-we 5075 |
. . . . . 6
|
115 | 112, 113,
114 | sylanbrc 698 |
. . . . 5
FinII
|
116 | | weinxp 5186 |
. . . . 5
|
117 | 115, 116 | sylib 208 |
. . . 4
FinII
|
118 | | sqxpexg 6963 |
. . . . . 6
FinII |
119 | | incom 3805 |
. . . . . . 7
|
120 | | inex1g 4801 |
. . . . . . 7
|
121 | 119, 120 | syl5eqel 2705 |
. . . . . 6
|
122 | | weeq1 5102 |
. . . . . . 7
|
123 | 122 | spcegv 3294 |
. . . . . 6
|
124 | 118, 121,
123 | 3syl 18 |
. . . . 5
FinII
|
125 | 124 | imp 445 |
. . . 4
FinII
|
126 | 117, 125 | syldan 487 |
. . 3
FinII
|
127 | | ween 8858 |
. . 3
|
128 | 126, 127 | sylibr 224 |
. 2
FinII
|
129 | | fin23 9211 |
. . . . 5
FinII FinIII |
130 | | fin34 9212 |
. . . . 5
FinIII FinIV |
131 | | fin45 9214 |
. . . . 5
FinIV FinV |
132 | 129, 130,
131 | 3syl 18 |
. . . 4
FinII FinV |
133 | | fin56 9215 |
. . . 4
FinV FinVI |
134 | | fin67 9217 |
. . . 4
FinVI FinVII |
135 | 132, 133,
134 | 3syl 18 |
. . 3
FinII FinVII |
136 | | fin71num 9219 |
. . . 4
FinVII |
137 | 136 | biimpac 503 |
. . 3
FinVII
|
138 | 135, 137 | sylan 488 |
. 2
FinII
|
139 | 128, 138 | syldan 487 |
1
FinII
|