Step | Hyp | Ref
| Expression |
1 | | bren 7964 |
. . 3
|
2 | | elpwi 4168 |
. . . . . . 7
|
3 | | imauni 6504 |
. . . . . . . . . . 11
|
4 | | vex 3203 |
. . . . . . . . . . . . 13
|
5 | 4 | imaex 7104 |
. . . . . . . . . . . 12
|
6 | 5 | dfiun2 4554 |
. . . . . . . . . . 11
|
7 | 3, 6 | eqtri 2644 |
. . . . . . . . . 10
|
8 | | imaeq2 5462 |
. . . . . . . . . . . . . . 15
|
9 | 8 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
10 | 9 | rexrab 3370 |
. . . . . . . . . . . . 13
|
11 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
12 | 11 | biimparc 504 |
. . . . . . . . . . . . . . 15
|
13 | 12 | rexlimivw 3029 |
. . . . . . . . . . . . . 14
|
14 | | cnvimass 5485 |
. . . . . . . . . . . . . . . . . 18
|
15 | | f1odm 6141 |
. . . . . . . . . . . . . . . . . . 19
|
16 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
FinII
[]
|
17 | 14, 16 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . 17
FinII
[]
|
18 | 4 | cnvex 7113 |
. . . . . . . . . . . . . . . . . . 19
|
19 | 18 | imaex 7104 |
. . . . . . . . . . . . . . . . . 18
|
20 | 19 | elpw 4164 |
. . . . . . . . . . . . . . . . 17
|
21 | 17, 20 | sylibr 224 |
. . . . . . . . . . . . . . . 16
FinII
[]
|
22 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . . . . 20
|
23 | 22 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
FinII
[]
|
24 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
FinII
[] |
25 | 24 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
FinII
[]
|
26 | 25 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . 19
FinII
[]
|
27 | | foimacnv 6154 |
. . . . . . . . . . . . . . . . . . 19
|
28 | 23, 26, 27 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
FinII
[]
|
29 | 28 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
FinII
[]
|
30 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
FinII
[]
|
31 | 29, 30 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
FinII
[]
|
32 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
|
34 | 32 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
35 | 33, 34 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | rspcev 3309 |
. . . . . . . . . . . . . . . 16
|
37 | 21, 31, 29, 36 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
FinII
[]
|
38 | 37 | ex 450 |
. . . . . . . . . . . . . 14
FinII
[] |
39 | 13, 38 | impbid2 216 |
. . . . . . . . . . . . 13
FinII
[]
|
40 | 10, 39 | syl5bb 272 |
. . . . . . . . . . . 12
FinII
[]
|
41 | 40 | abbi1dv 2743 |
. . . . . . . . . . 11
FinII
[]
|
42 | 41 | unieqd 4446 |
. . . . . . . . . 10
FinII
[]
|
43 | 7, 42 | syl5eq 2668 |
. . . . . . . . 9
FinII
[]
|
44 | | simplr 792 |
. . . . . . . . . . 11
FinII
[]
FinII |
45 | | ssrab2 3687 |
. . . . . . . . . . . 12
|
46 | 45 | a1i 11 |
. . . . . . . . . . 11
FinII
[]
|
47 | | simprrl 804 |
. . . . . . . . . . . . . 14
FinII
[] |
48 | | n0 3931 |
. . . . . . . . . . . . . 14
|
49 | 47, 48 | sylib 208 |
. . . . . . . . . . . . 13
FinII
[]
|
50 | | imaeq2 5462 |
. . . . . . . . . . . . . . . 16
|
51 | 50 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
|
52 | 51 | rspcev 3309 |
. . . . . . . . . . . . . 14
|
53 | 21, 31, 52 | syl2anc 693 |
. . . . . . . . . . . . 13
FinII
[]
|
54 | 49, 53 | exlimddv 1863 |
. . . . . . . . . . . 12
FinII
[]
|
55 | | rabn0 3958 |
. . . . . . . . . . . 12
|
56 | 54, 55 | sylibr 224 |
. . . . . . . . . . 11
FinII
[]
|
57 | 9 | elrab 3363 |
. . . . . . . . . . . . . . 15
|
58 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
60 | 59 | elrab 3363 |
. . . . . . . . . . . . . . 15
|
61 | 57, 60 | anbi12i 733 |
. . . . . . . . . . . . . 14
|
62 | | simprrr 805 |
. . . . . . . . . . . . . . . . 17
FinII
[] [] |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . 16
FinII
[]
[] |
64 | | simprlr 803 |
. . . . . . . . . . . . . . . 16
FinII
[]
|
65 | | simprrr 805 |
. . . . . . . . . . . . . . . 16
FinII
[]
|
66 | | sorpssi 6943 |
. . . . . . . . . . . . . . . 16
[]
|
67 | 63, 64, 65, 66 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
FinII
[]
|
68 | | f1of1 6136 |
. . . . . . . . . . . . . . . . . 18
|
69 | 68 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
FinII
[]
|
70 | | simprll 802 |
. . . . . . . . . . . . . . . . . 18
FinII
[]
|
71 | 70 | elpwid 4170 |
. . . . . . . . . . . . . . . . 17
FinII
[]
|
72 | | simprrl 804 |
. . . . . . . . . . . . . . . . . 18
FinII
[]
|
73 | 72 | elpwid 4170 |
. . . . . . . . . . . . . . . . 17
FinII
[]
|
74 | | f1imass 6521 |
. . . . . . . . . . . . . . . . 17
|
75 | 69, 71, 73, 74 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
FinII
[]
|
76 | | f1imass 6521 |
. . . . . . . . . . . . . . . . 17
|
77 | 69, 73, 71, 76 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
FinII
[]
|
78 | 75, 77 | orbi12d 746 |
. . . . . . . . . . . . . . 15
FinII
[]
|
79 | 67, 78 | mpbid 222 |
. . . . . . . . . . . . . 14
FinII
[]
|
80 | 61, 79 | sylan2b 492 |
. . . . . . . . . . . . 13
FinII
[]
|
81 | 80 | ralrimivva 2971 |
. . . . . . . . . . . 12
FinII
[]
|
82 | | sorpss 6942 |
. . . . . . . . . . . 12
[]
|
83 | 81, 82 | sylibr 224 |
. . . . . . . . . . 11
FinII
[] [] |
84 | | fin2i 9117 |
. . . . . . . . . . 11
FinII
[]
|
85 | 44, 46, 56, 83, 84 | syl22anc 1327 |
. . . . . . . . . 10
FinII
[]
|
86 | | imaeq2 5462 |
. . . . . . . . . . . . 13
|
87 | 86 | eleq1d 2686 |
. . . . . . . . . . . 12
|
88 | 9 | cbvrabv 3199 |
. . . . . . . . . . . 12
|
89 | 87, 88 | elrab2 3366 |
. . . . . . . . . . 11
|
90 | 89 | simprbi 480 |
. . . . . . . . . 10
|
91 | 85, 90 | syl 17 |
. . . . . . . . 9
FinII
[]
|
92 | 43, 91 | eqeltrrd 2702 |
. . . . . . . 8
FinII
[]
|
93 | 92 | expr 643 |
. . . . . . 7
FinII
[]
|
94 | 2, 93 | sylan2 491 |
. . . . . 6
FinII
[]
|
95 | 94 | ralrimiva 2966 |
. . . . 5
FinII []
|
96 | 95 | ex 450 |
. . . 4
FinII
[]
|
97 | 96 | exlimiv 1858 |
. . 3
FinII []
|
98 | 1, 97 | sylbi 207 |
. 2
FinII
[]
|
99 | | relen 7960 |
. . . 4
|
100 | 99 | brrelex2i 5159 |
. . 3
|
101 | | isfin2 9116 |
. . 3
FinII
[]
|
102 | 100, 101 | syl 17 |
. 2
FinII
[]
|
103 | 98, 102 | sylibrd 249 |
1
FinII FinII |