Step | Hyp | Ref
| Expression |
1 | | bren 6725 |
. . 3
|
2 | | f1odm 5446 |
. . . . . . 7
|
3 | | vex 2733 |
. . . . . . . 8
|
4 | 3 | dmex 4877 |
. . . . . . 7
|
5 | 2, 4 | eqeltrrdi 2262 |
. . . . . 6
|
6 | | pwexg 4166 |
. . . . . 6
|
7 | | inex1g 4125 |
. . . . . 6
|
8 | 5, 6, 7 | 3syl 17 |
. . . . 5
|
9 | | f1ofo 5449 |
. . . . . . . 8
|
10 | | forn 5423 |
. . . . . . . 8
|
11 | 9, 10 | syl 14 |
. . . . . . 7
|
12 | 3 | rnex 4878 |
. . . . . . 7
|
13 | 11, 12 | eqeltrrdi 2262 |
. . . . . 6
|
14 | | pwexg 4166 |
. . . . . 6
|
15 | | inex1g 4125 |
. . . . . 6
|
16 | 13, 14, 15 | 3syl 17 |
. . . . 5
|
17 | | f1of1 5441 |
. . . . . . . . . . 11
|
18 | 17 | adantr 274 |
. . . . . . . . . 10
|
19 | 13 | adantr 274 |
. . . . . . . . . 10
|
20 | | simpr 109 |
. . . . . . . . . 10
|
21 | | vex 2733 |
. . . . . . . . . . 11
|
22 | 21 | a1i 9 |
. . . . . . . . . 10
|
23 | | f1imaen2g 6771 |
. . . . . . . . . 10
|
24 | 18, 19, 20, 22, 23 | syl22anc 1234 |
. . . . . . . . 9
|
25 | | entr 6762 |
. . . . . . . . 9
|
26 | 24, 25 | sylan 281 |
. . . . . . . 8
|
27 | 26 | expl 376 |
. . . . . . 7
|
28 | | imassrn 4964 |
. . . . . . . . 9
|
29 | 28, 10 | sseqtrid 3197 |
. . . . . . . 8
|
30 | 9, 29 | syl 14 |
. . . . . . 7
|
31 | 27, 30 | jctild 314 |
. . . . . 6
|
32 | | elin 3310 |
. . . . . . 7
|
33 | 21 | elpw 3572 |
. . . . . . . 8
|
34 | | breq1 3992 |
. . . . . . . . 9
|
35 | 21, 34 | elab 2874 |
. . . . . . . 8
|
36 | 33, 35 | anbi12i 457 |
. . . . . . 7
|
37 | 32, 36 | bitri 183 |
. . . . . 6
|
38 | | elin 3310 |
. . . . . . 7
|
39 | 3 | imaex 4966 |
. . . . . . . . 9
|
40 | 39 | elpw 3572 |
. . . . . . . 8
|
41 | | breq1 3992 |
. . . . . . . . 9
|
42 | 39, 41 | elab 2874 |
. . . . . . . 8
|
43 | 40, 42 | anbi12i 457 |
. . . . . . 7
|
44 | 38, 43 | bitri 183 |
. . . . . 6
|
45 | 31, 37, 44 | 3imtr4g 204 |
. . . . 5
|
46 | | f1ocnv 5455 |
. . . . . . 7
|
47 | | f1of1 5441 |
. . . . . . . . . . . 12
|
48 | | f1f1orn 5453 |
. . . . . . . . . . . 12
|
49 | | f1of1 5441 |
. . . . . . . . . . . 12
|
50 | 47, 48, 49 | 3syl 17 |
. . . . . . . . . . 11
|
51 | | vex 2733 |
. . . . . . . . . . . 12
|
52 | 51 | f1imaen 6772 |
. . . . . . . . . . 11
|
53 | 50, 52 | sylan 281 |
. . . . . . . . . 10
|
54 | | entr 6762 |
. . . . . . . . . 10
|
55 | 53, 54 | sylan 281 |
. . . . . . . . 9
|
56 | 55 | expl 376 |
. . . . . . . 8
|
57 | | f1ofo 5449 |
. . . . . . . . 9
|
58 | | imassrn 4964 |
. . . . . . . . . 10
|
59 | | forn 5423 |
. . . . . . . . . 10
|
60 | 58, 59 | sseqtrid 3197 |
. . . . . . . . 9
|
61 | 57, 60 | syl 14 |
. . . . . . . 8
|
62 | 56, 61 | jctild 314 |
. . . . . . 7
|
63 | 46, 62 | syl 14 |
. . . . . 6
|
64 | | elin 3310 |
. . . . . . 7
|
65 | 51 | elpw 3572 |
. . . . . . . 8
|
66 | | breq1 3992 |
. . . . . . . . 9
|
67 | 51, 66 | elab 2874 |
. . . . . . . 8
|
68 | 65, 67 | anbi12i 457 |
. . . . . . 7
|
69 | 64, 68 | bitri 183 |
. . . . . 6
|
70 | | elin 3310 |
. . . . . . 7
|
71 | 3 | cnvex 5149 |
. . . . . . . . . 10
|
72 | 71 | imaex 4966 |
. . . . . . . . 9
|
73 | 72 | elpw 3572 |
. . . . . . . 8
|
74 | | breq1 3992 |
. . . . . . . . 9
|
75 | 72, 74 | elab 2874 |
. . . . . . . 8
|
76 | 73, 75 | anbi12i 457 |
. . . . . . 7
|
77 | 70, 76 | bitri 183 |
. . . . . 6
|
78 | 63, 69, 77 | 3imtr4g 204 |
. . . . 5
|
79 | | simpl 108 |
. . . . . . . . . . 11
|
80 | 79 | elpwid 3577 |
. . . . . . . . . 10
|
81 | 64, 80 | sylbi 120 |
. . . . . . . . 9
|
82 | | imaeq2 4949 |
. . . . . . . . . . . 12
|
83 | | f1orel 5445 |
. . . . . . . . . . . . . . . 16
|
84 | | dfrel2 5061 |
. . . . . . . . . . . . . . . 16
|
85 | 83, 84 | sylib 121 |
. . . . . . . . . . . . . . 15
|
86 | 85 | imaeq1d 4952 |
. . . . . . . . . . . . . 14
|
87 | 86 | adantr 274 |
. . . . . . . . . . . . 13
|
88 | 46, 47 | syl 14 |
. . . . . . . . . . . . . 14
|
89 | | f1imacnv 5459 |
. . . . . . . . . . . . . 14
|
90 | 88, 89 | sylan 281 |
. . . . . . . . . . . . 13
|
91 | 87, 90 | eqtr3d 2205 |
. . . . . . . . . . . 12
|
92 | 82, 91 | sylan9eqr 2225 |
. . . . . . . . . . 11
|
93 | 92 | eqcomd 2176 |
. . . . . . . . . 10
|
94 | 93 | ex 114 |
. . . . . . . . 9
|
95 | 81, 94 | sylan2 284 |
. . . . . . . 8
|
96 | 95 | adantrl 475 |
. . . . . . 7
|
97 | | simpl 108 |
. . . . . . . . . . 11
|
98 | 97 | elpwid 3577 |
. . . . . . . . . 10
|
99 | 32, 98 | sylbi 120 |
. . . . . . . . 9
|
100 | | imaeq2 4949 |
. . . . . . . . . . . 12
|
101 | | f1imacnv 5459 |
. . . . . . . . . . . . 13
|
102 | 17, 101 | sylan 281 |
. . . . . . . . . . . 12
|
103 | 100, 102 | sylan9eqr 2225 |
. . . . . . . . . . 11
|
104 | 103 | eqcomd 2176 |
. . . . . . . . . 10
|
105 | 104 | ex 114 |
. . . . . . . . 9
|
106 | 99, 105 | sylan2 284 |
. . . . . . . 8
|
107 | 106 | adantrr 476 |
. . . . . . 7
|
108 | 96, 107 | impbid 128 |
. . . . . 6
|
109 | 108 | ex 114 |
. . . . 5
|
110 | 8, 16, 45, 78, 109 | en3d 6747 |
. . . 4
|
111 | 110 | exlimiv 1591 |
. . 3
|
112 | 1, 111 | sylbi 120 |
. 2
|
113 | | df-pw 3568 |
. . . 4
|
114 | 113 | ineq1i 3324 |
. . 3
|
115 | | inab 3395 |
. . 3
|
116 | 114, 115 | eqtri 2191 |
. 2
|
117 | | df-pw 3568 |
. . . 4
|
118 | 117 | ineq1i 3324 |
. . 3
|
119 | | inab 3395 |
. . 3
|
120 | 118, 119 | eqtri 2191 |
. 2
|
121 | 112, 116,
120 | 3brtr3g 4022 |
1
|