Step | Hyp | Ref
| Expression |
1 | | bren 6692 |
. . 3
|
2 | | f1odm 5418 |
. . . . . . 7
|
3 | | vex 2715 |
. . . . . . . 8
|
4 | 3 | dmex 4852 |
. . . . . . 7
|
5 | 2, 4 | eqeltrrdi 2249 |
. . . . . 6
|
6 | | pwexg 4141 |
. . . . . 6
|
7 | | inex1g 4100 |
. . . . . 6
|
8 | 5, 6, 7 | 3syl 17 |
. . . . 5
|
9 | | f1ofo 5421 |
. . . . . . . 8
|
10 | | forn 5395 |
. . . . . . . 8
|
11 | 9, 10 | syl 14 |
. . . . . . 7
|
12 | 3 | rnex 4853 |
. . . . . . 7
|
13 | 11, 12 | eqeltrrdi 2249 |
. . . . . 6
|
14 | | pwexg 4141 |
. . . . . 6
|
15 | | inex1g 4100 |
. . . . . 6
|
16 | 13, 14, 15 | 3syl 17 |
. . . . 5
|
17 | | f1of1 5413 |
. . . . . . . . . . 11
|
18 | 17 | adantr 274 |
. . . . . . . . . 10
|
19 | 13 | adantr 274 |
. . . . . . . . . 10
|
20 | | simpr 109 |
. . . . . . . . . 10
|
21 | | vex 2715 |
. . . . . . . . . . 11
|
22 | 21 | a1i 9 |
. . . . . . . . . 10
|
23 | | f1imaen2g 6738 |
. . . . . . . . . 10
|
24 | 18, 19, 20, 22, 23 | syl22anc 1221 |
. . . . . . . . 9
|
25 | | entr 6729 |
. . . . . . . . 9
|
26 | 24, 25 | sylan 281 |
. . . . . . . 8
|
27 | 26 | expl 376 |
. . . . . . 7
|
28 | | imassrn 4939 |
. . . . . . . . 9
|
29 | 28, 10 | sseqtrid 3178 |
. . . . . . . 8
|
30 | 9, 29 | syl 14 |
. . . . . . 7
|
31 | 27, 30 | jctild 314 |
. . . . . 6
|
32 | | elin 3290 |
. . . . . . 7
|
33 | 21 | elpw 3549 |
. . . . . . . 8
|
34 | | breq1 3968 |
. . . . . . . . 9
|
35 | 21, 34 | elab 2856 |
. . . . . . . 8
|
36 | 33, 35 | anbi12i 456 |
. . . . . . 7
|
37 | 32, 36 | bitri 183 |
. . . . . 6
|
38 | | elin 3290 |
. . . . . . 7
|
39 | 3 | imaex 4941 |
. . . . . . . . 9
|
40 | 39 | elpw 3549 |
. . . . . . . 8
|
41 | | breq1 3968 |
. . . . . . . . 9
|
42 | 39, 41 | elab 2856 |
. . . . . . . 8
|
43 | 40, 42 | anbi12i 456 |
. . . . . . 7
|
44 | 38, 43 | bitri 183 |
. . . . . 6
|
45 | 31, 37, 44 | 3imtr4g 204 |
. . . . 5
|
46 | | f1ocnv 5427 |
. . . . . . 7
|
47 | | f1of1 5413 |
. . . . . . . . . . . 12
|
48 | | f1f1orn 5425 |
. . . . . . . . . . . 12
|
49 | | f1of1 5413 |
. . . . . . . . . . . 12
|
50 | 47, 48, 49 | 3syl 17 |
. . . . . . . . . . 11
|
51 | | vex 2715 |
. . . . . . . . . . . 12
|
52 | 51 | f1imaen 6739 |
. . . . . . . . . . 11
|
53 | 50, 52 | sylan 281 |
. . . . . . . . . 10
|
54 | | entr 6729 |
. . . . . . . . . 10
|
55 | 53, 54 | sylan 281 |
. . . . . . . . 9
|
56 | 55 | expl 376 |
. . . . . . . 8
|
57 | | f1ofo 5421 |
. . . . . . . . 9
|
58 | | imassrn 4939 |
. . . . . . . . . 10
|
59 | | forn 5395 |
. . . . . . . . . 10
|
60 | 58, 59 | sseqtrid 3178 |
. . . . . . . . 9
|
61 | 57, 60 | syl 14 |
. . . . . . . 8
|
62 | 56, 61 | jctild 314 |
. . . . . . 7
|
63 | 46, 62 | syl 14 |
. . . . . 6
|
64 | | elin 3290 |
. . . . . . 7
|
65 | 51 | elpw 3549 |
. . . . . . . 8
|
66 | | breq1 3968 |
. . . . . . . . 9
|
67 | 51, 66 | elab 2856 |
. . . . . . . 8
|
68 | 65, 67 | anbi12i 456 |
. . . . . . 7
|
69 | 64, 68 | bitri 183 |
. . . . . 6
|
70 | | elin 3290 |
. . . . . . 7
|
71 | 3 | cnvex 5124 |
. . . . . . . . . 10
|
72 | 71 | imaex 4941 |
. . . . . . . . 9
|
73 | 72 | elpw 3549 |
. . . . . . . 8
|
74 | | breq1 3968 |
. . . . . . . . 9
|
75 | 72, 74 | elab 2856 |
. . . . . . . 8
|
76 | 73, 75 | anbi12i 456 |
. . . . . . 7
|
77 | 70, 76 | bitri 183 |
. . . . . 6
|
78 | 63, 69, 77 | 3imtr4g 204 |
. . . . 5
|
79 | | simpl 108 |
. . . . . . . . . . 11
|
80 | 79 | elpwid 3554 |
. . . . . . . . . 10
|
81 | 64, 80 | sylbi 120 |
. . . . . . . . 9
|
82 | | imaeq2 4924 |
. . . . . . . . . . . 12
|
83 | | f1orel 5417 |
. . . . . . . . . . . . . . . 16
|
84 | | dfrel2 5036 |
. . . . . . . . . . . . . . . 16
|
85 | 83, 84 | sylib 121 |
. . . . . . . . . . . . . . 15
|
86 | 85 | imaeq1d 4927 |
. . . . . . . . . . . . . 14
|
87 | 86 | adantr 274 |
. . . . . . . . . . . . 13
|
88 | 46, 47 | syl 14 |
. . . . . . . . . . . . . 14
|
89 | | f1imacnv 5431 |
. . . . . . . . . . . . . 14
|
90 | 88, 89 | sylan 281 |
. . . . . . . . . . . . 13
|
91 | 87, 90 | eqtr3d 2192 |
. . . . . . . . . . . 12
|
92 | 82, 91 | sylan9eqr 2212 |
. . . . . . . . . . 11
|
93 | 92 | eqcomd 2163 |
. . . . . . . . . 10
|
94 | 93 | ex 114 |
. . . . . . . . 9
|
95 | 81, 94 | sylan2 284 |
. . . . . . . 8
|
96 | 95 | adantrl 470 |
. . . . . . 7
|
97 | | simpl 108 |
. . . . . . . . . . 11
|
98 | 97 | elpwid 3554 |
. . . . . . . . . 10
|
99 | 32, 98 | sylbi 120 |
. . . . . . . . 9
|
100 | | imaeq2 4924 |
. . . . . . . . . . . 12
|
101 | | f1imacnv 5431 |
. . . . . . . . . . . . 13
|
102 | 17, 101 | sylan 281 |
. . . . . . . . . . . 12
|
103 | 100, 102 | sylan9eqr 2212 |
. . . . . . . . . . 11
|
104 | 103 | eqcomd 2163 |
. . . . . . . . . 10
|
105 | 104 | ex 114 |
. . . . . . . . 9
|
106 | 99, 105 | sylan2 284 |
. . . . . . . 8
|
107 | 106 | adantrr 471 |
. . . . . . 7
|
108 | 96, 107 | impbid 128 |
. . . . . 6
|
109 | 108 | ex 114 |
. . . . 5
|
110 | 8, 16, 45, 78, 109 | en3d 6714 |
. . . 4
|
111 | 110 | exlimiv 1578 |
. . 3
|
112 | 1, 111 | sylbi 120 |
. 2
|
113 | | df-pw 3545 |
. . . 4
|
114 | 113 | ineq1i 3304 |
. . 3
|
115 | | inab 3375 |
. . 3
|
116 | 114, 115 | eqtri 2178 |
. 2
|
117 | | df-pw 3545 |
. . . 4
|
118 | 117 | ineq1i 3304 |
. . 3
|
119 | | inab 3375 |
. . 3
|
120 | 118, 119 | eqtri 2178 |
. 2
|
121 | 112, 116,
120 | 3brtr3g 3997 |
1
|