Step | Hyp | Ref
| Expression |
1 | | bren 6609 |
. . 3
|
2 | | f1odm 5339 |
. . . . . . 7
|
3 | | vex 2663 |
. . . . . . . 8
|
4 | 3 | dmex 4775 |
. . . . . . 7
|
5 | 2, 4 | syl6eqelr 2209 |
. . . . . 6
|
6 | | pwexg 4074 |
. . . . . 6
|
7 | | inex1g 4034 |
. . . . . 6
|
8 | 5, 6, 7 | 3syl 17 |
. . . . 5
|
9 | | f1ofo 5342 |
. . . . . . . 8
|
10 | | forn 5318 |
. . . . . . . 8
|
11 | 9, 10 | syl 14 |
. . . . . . 7
|
12 | 3 | rnex 4776 |
. . . . . . 7
|
13 | 11, 12 | syl6eqelr 2209 |
. . . . . 6
|
14 | | pwexg 4074 |
. . . . . 6
|
15 | | inex1g 4034 |
. . . . . 6
|
16 | 13, 14, 15 | 3syl 17 |
. . . . 5
|
17 | | f1of1 5334 |
. . . . . . . . . . 11
|
18 | 17 | adantr 274 |
. . . . . . . . . 10
|
19 | 13 | adantr 274 |
. . . . . . . . . 10
|
20 | | simpr 109 |
. . . . . . . . . 10
|
21 | | vex 2663 |
. . . . . . . . . . 11
|
22 | 21 | a1i 9 |
. . . . . . . . . 10
|
23 | | f1imaen2g 6655 |
. . . . . . . . . 10
|
24 | 18, 19, 20, 22, 23 | syl22anc 1202 |
. . . . . . . . 9
|
25 | | entr 6646 |
. . . . . . . . 9
|
26 | 24, 25 | sylan 281 |
. . . . . . . 8
|
27 | 26 | expl 375 |
. . . . . . 7
|
28 | | imassrn 4862 |
. . . . . . . . 9
|
29 | 28, 10 | sseqtrid 3117 |
. . . . . . . 8
|
30 | 9, 29 | syl 14 |
. . . . . . 7
|
31 | 27, 30 | jctild 314 |
. . . . . 6
|
32 | | elin 3229 |
. . . . . . 7
|
33 | 21 | elpw 3486 |
. . . . . . . 8
|
34 | | breq1 3902 |
. . . . . . . . 9
|
35 | 21, 34 | elab 2802 |
. . . . . . . 8
|
36 | 33, 35 | anbi12i 455 |
. . . . . . 7
|
37 | 32, 36 | bitri 183 |
. . . . . 6
|
38 | | elin 3229 |
. . . . . . 7
|
39 | 3 | imaex 4864 |
. . . . . . . . 9
|
40 | 39 | elpw 3486 |
. . . . . . . 8
|
41 | | breq1 3902 |
. . . . . . . . 9
|
42 | 39, 41 | elab 2802 |
. . . . . . . 8
|
43 | 40, 42 | anbi12i 455 |
. . . . . . 7
|
44 | 38, 43 | bitri 183 |
. . . . . 6
|
45 | 31, 37, 44 | 3imtr4g 204 |
. . . . 5
|
46 | | f1ocnv 5348 |
. . . . . . 7
|
47 | | f1of1 5334 |
. . . . . . . . . . . 12
|
48 | | f1f1orn 5346 |
. . . . . . . . . . . 12
|
49 | | f1of1 5334 |
. . . . . . . . . . . 12
|
50 | 47, 48, 49 | 3syl 17 |
. . . . . . . . . . 11
|
51 | | vex 2663 |
. . . . . . . . . . . 12
|
52 | 51 | f1imaen 6656 |
. . . . . . . . . . 11
|
53 | 50, 52 | sylan 281 |
. . . . . . . . . 10
|
54 | | entr 6646 |
. . . . . . . . . 10
|
55 | 53, 54 | sylan 281 |
. . . . . . . . 9
|
56 | 55 | expl 375 |
. . . . . . . 8
|
57 | | f1ofo 5342 |
. . . . . . . . 9
|
58 | | imassrn 4862 |
. . . . . . . . . 10
|
59 | | forn 5318 |
. . . . . . . . . 10
|
60 | 58, 59 | sseqtrid 3117 |
. . . . . . . . 9
|
61 | 57, 60 | syl 14 |
. . . . . . . 8
|
62 | 56, 61 | jctild 314 |
. . . . . . 7
|
63 | 46, 62 | syl 14 |
. . . . . 6
|
64 | | elin 3229 |
. . . . . . 7
|
65 | 51 | elpw 3486 |
. . . . . . . 8
|
66 | | breq1 3902 |
. . . . . . . . 9
|
67 | 51, 66 | elab 2802 |
. . . . . . . 8
|
68 | 65, 67 | anbi12i 455 |
. . . . . . 7
|
69 | 64, 68 | bitri 183 |
. . . . . 6
|
70 | | elin 3229 |
. . . . . . 7
|
71 | 3 | cnvex 5047 |
. . . . . . . . . 10
|
72 | 71 | imaex 4864 |
. . . . . . . . 9
|
73 | 72 | elpw 3486 |
. . . . . . . 8
|
74 | | breq1 3902 |
. . . . . . . . 9
|
75 | 72, 74 | elab 2802 |
. . . . . . . 8
|
76 | 73, 75 | anbi12i 455 |
. . . . . . 7
|
77 | 70, 76 | bitri 183 |
. . . . . 6
|
78 | 63, 69, 77 | 3imtr4g 204 |
. . . . 5
|
79 | | simpl 108 |
. . . . . . . . . . 11
|
80 | 79 | elpwid 3491 |
. . . . . . . . . 10
|
81 | 64, 80 | sylbi 120 |
. . . . . . . . 9
|
82 | | imaeq2 4847 |
. . . . . . . . . . . 12
|
83 | | f1orel 5338 |
. . . . . . . . . . . . . . . 16
|
84 | | dfrel2 4959 |
. . . . . . . . . . . . . . . 16
|
85 | 83, 84 | sylib 121 |
. . . . . . . . . . . . . . 15
|
86 | 85 | imaeq1d 4850 |
. . . . . . . . . . . . . 14
|
87 | 86 | adantr 274 |
. . . . . . . . . . . . 13
|
88 | 46, 47 | syl 14 |
. . . . . . . . . . . . . 14
|
89 | | f1imacnv 5352 |
. . . . . . . . . . . . . 14
|
90 | 88, 89 | sylan 281 |
. . . . . . . . . . . . 13
|
91 | 87, 90 | eqtr3d 2152 |
. . . . . . . . . . . 12
|
92 | 82, 91 | sylan9eqr 2172 |
. . . . . . . . . . 11
|
93 | 92 | eqcomd 2123 |
. . . . . . . . . 10
|
94 | 93 | ex 114 |
. . . . . . . . 9
|
95 | 81, 94 | sylan2 284 |
. . . . . . . 8
|
96 | 95 | adantrl 469 |
. . . . . . 7
|
97 | | simpl 108 |
. . . . . . . . . . 11
|
98 | 97 | elpwid 3491 |
. . . . . . . . . 10
|
99 | 32, 98 | sylbi 120 |
. . . . . . . . 9
|
100 | | imaeq2 4847 |
. . . . . . . . . . . 12
|
101 | | f1imacnv 5352 |
. . . . . . . . . . . . 13
|
102 | 17, 101 | sylan 281 |
. . . . . . . . . . . 12
|
103 | 100, 102 | sylan9eqr 2172 |
. . . . . . . . . . 11
|
104 | 103 | eqcomd 2123 |
. . . . . . . . . 10
|
105 | 104 | ex 114 |
. . . . . . . . 9
|
106 | 99, 105 | sylan2 284 |
. . . . . . . 8
|
107 | 106 | adantrr 470 |
. . . . . . 7
|
108 | 96, 107 | impbid 128 |
. . . . . 6
|
109 | 108 | ex 114 |
. . . . 5
|
110 | 8, 16, 45, 78, 109 | en3d 6631 |
. . . 4
|
111 | 110 | exlimiv 1562 |
. . 3
|
112 | 1, 111 | sylbi 120 |
. 2
|
113 | | df-pw 3482 |
. . . 4
|
114 | 113 | ineq1i 3243 |
. . 3
|
115 | | inab 3314 |
. . 3
|
116 | 114, 115 | eqtri 2138 |
. 2
|
117 | | df-pw 3482 |
. . . 4
|
118 | 117 | ineq1i 3243 |
. . 3
|
119 | | inab 3314 |
. . 3
|
120 | 118, 119 | eqtri 2138 |
. 2
|
121 | 112, 116,
120 | 3brtr3g 3931 |
1
|