Step | Hyp | Ref
| Expression |
1 | | bren 7964 |
. 2
|
2 | | bren 7964 |
. 2
|
3 | | eeanv 2182 |
. . 3
|
4 | | f1of 6137 |
. . . . . . . 8
|
5 | | f1odm 6141 |
. . . . . . . . . 10
|
6 | | vex 3203 |
. . . . . . . . . . 11
|
7 | 6 | dmex 7099 |
. . . . . . . . . 10
|
8 | 5, 7 | syl6eqelr 2710 |
. . . . . . . . 9
|
9 | | f1odm 6141 |
. . . . . . . . . 10
|
10 | | vex 3203 |
. . . . . . . . . . 11
|
11 | 10 | dmex 7099 |
. . . . . . . . . 10
|
12 | 9, 11 | syl6eqelr 2710 |
. . . . . . . . 9
|
13 | | elmapg 7870 |
. . . . . . . . 9
|
14 | 8, 12, 13 | syl2anr 495 |
. . . . . . . 8
|
15 | 4, 14 | syl5ibr 236 |
. . . . . . 7
|
16 | 15 | abssdv 3676 |
. . . . . 6
|
17 | | ovex 6678 |
. . . . . . 7
|
18 | 17 | ssex 4802 |
. . . . . 6
|
19 | 16, 18 | syl 17 |
. . . . 5
|
20 | | f1of 6137 |
. . . . . . . 8
|
21 | | f1ofo 6144 |
. . . . . . . . . . 11
|
22 | | forn 6118 |
. . . . . . . . . . 11
|
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
|
24 | 6 | rnex 7100 |
. . . . . . . . . 10
|
25 | 23, 24 | syl6eqelr 2710 |
. . . . . . . . 9
|
26 | | f1ofo 6144 |
. . . . . . . . . . 11
|
27 | | forn 6118 |
. . . . . . . . . . 11
|
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
|
29 | 10 | rnex 7100 |
. . . . . . . . . 10
|
30 | 28, 29 | syl6eqelr 2710 |
. . . . . . . . 9
|
31 | | elmapg 7870 |
. . . . . . . . 9
|
32 | 25, 30, 31 | syl2anr 495 |
. . . . . . . 8
|
33 | 20, 32 | syl5ibr 236 |
. . . . . . 7
|
34 | 33 | abssdv 3676 |
. . . . . 6
|
35 | | ovex 6678 |
. . . . . . 7
|
36 | 35 | ssex 4802 |
. . . . . 6
|
37 | 34, 36 | syl 17 |
. . . . 5
|
38 | | f1oco 6159 |
. . . . . . . . 9
|
39 | 38 | adantll 750 |
. . . . . . . 8
|
40 | | f1ocnv 6149 |
. . . . . . . . 9
|
41 | 40 | ad2antrr 762 |
. . . . . . . 8
|
42 | | f1oco 6159 |
. . . . . . . 8
|
43 | 39, 41, 42 | syl2anc 693 |
. . . . . . 7
|
44 | 43 | ex 450 |
. . . . . 6
|
45 | | vex 3203 |
. . . . . . 7
|
46 | | f1oeq1 6127 |
. . . . . . 7
|
47 | 45, 46 | elab 3350 |
. . . . . 6
|
48 | 6, 45 | coex 7118 |
. . . . . . . 8
|
49 | 10 | cnvex 7113 |
. . . . . . . 8
|
50 | 48, 49 | coex 7118 |
. . . . . . 7
|
51 | | f1oeq1 6127 |
. . . . . . 7
|
52 | 50, 51 | elab 3350 |
. . . . . 6
|
53 | 44, 47, 52 | 3imtr4g 285 |
. . . . 5
|
54 | | f1ocnv 6149 |
. . . . . . . . 9
|
55 | 54 | ad2antlr 763 |
. . . . . . . 8
|
56 | | f1oco 6159 |
. . . . . . . . . 10
|
57 | 56 | ancoms 469 |
. . . . . . . . 9
|
58 | 57 | adantlr 751 |
. . . . . . . 8
|
59 | | f1oco 6159 |
. . . . . . . 8
|
60 | 55, 58, 59 | syl2anc 693 |
. . . . . . 7
|
61 | 60 | ex 450 |
. . . . . 6
|
62 | | vex 3203 |
. . . . . . 7
|
63 | | f1oeq1 6127 |
. . . . . . 7
|
64 | 62, 63 | elab 3350 |
. . . . . 6
|
65 | 6 | cnvex 7113 |
. . . . . . . 8
|
66 | 62, 10 | coex 7118 |
. . . . . . . 8
|
67 | 65, 66 | coex 7118 |
. . . . . . 7
|
68 | | f1oeq1 6127 |
. . . . . . 7
|
69 | 67, 68 | elab 3350 |
. . . . . 6
|
70 | 61, 64, 69 | 3imtr4g 285 |
. . . . 5
|
71 | 47, 64 | anbi12i 733 |
. . . . . 6
|
72 | | coass 5654 |
. . . . . . . . . . 11
|
73 | | f1ococnv1 6165 |
. . . . . . . . . . . . . 14
|
74 | 73 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
75 | 74 | coeq2d 5284 |
. . . . . . . . . . . 12
|
76 | 39 | adantrr 753 |
. . . . . . . . . . . . 13
|
77 | | f1of 6137 |
. . . . . . . . . . . . 13
|
78 | | fcoi1 6078 |
. . . . . . . . . . . . 13
|
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . . . 12
|
80 | 75, 79 | eqtrd 2656 |
. . . . . . . . . . 11
|
81 | 72, 80 | syl5req 2669 |
. . . . . . . . . 10
|
82 | | coass 5654 |
. . . . . . . . . . 11
|
83 | | f1ococnv2 6163 |
. . . . . . . . . . . . . 14
|
84 | 83 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
85 | 84 | coeq1d 5283 |
. . . . . . . . . . . 12
|
86 | 58 | adantrl 752 |
. . . . . . . . . . . . 13
|
87 | | f1of 6137 |
. . . . . . . . . . . . 13
|
88 | | fcoi2 6079 |
. . . . . . . . . . . . 13
|
89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . 12
|
90 | 85, 89 | eqtrd 2656 |
. . . . . . . . . . 11
|
91 | 82, 90 | syl5eqr 2670 |
. . . . . . . . . 10
|
92 | 81, 91 | eqeq12d 2637 |
. . . . . . . . 9
|
93 | | eqcom 2629 |
. . . . . . . . 9
|
94 | 92, 93 | syl6bb 276 |
. . . . . . . 8
|
95 | | f1of1 6136 |
. . . . . . . . . 10
|
96 | 95 | ad2antlr 763 |
. . . . . . . . 9
|
97 | | f1of 6137 |
. . . . . . . . . 10
|
98 | 97 | ad2antrl 764 |
. . . . . . . . 9
|
99 | 60 | adantrl 752 |
. . . . . . . . . 10
|
100 | | f1of 6137 |
. . . . . . . . . 10
|
101 | 99, 100 | syl 17 |
. . . . . . . . 9
|
102 | | cocan1 6546 |
. . . . . . . . 9
|
103 | 96, 98, 101, 102 | syl3anc 1326 |
. . . . . . . 8
|
104 | 26 | ad2antrr 762 |
. . . . . . . . 9
|
105 | | f1ofn 6138 |
. . . . . . . . . 10
|
106 | 105 | ad2antll 765 |
. . . . . . . . 9
|
107 | 43 | adantrr 753 |
. . . . . . . . . 10
|
108 | | f1ofn 6138 |
. . . . . . . . . 10
|
109 | 107, 108 | syl 17 |
. . . . . . . . 9
|
110 | | cocan2 6547 |
. . . . . . . . 9
|
111 | 104, 106,
109, 110 | syl3anc 1326 |
. . . . . . . 8
|
112 | 94, 103, 111 | 3bitr3d 298 |
. . . . . . 7
|
113 | 112 | ex 450 |
. . . . . 6
|
114 | 71, 113 | syl5bi 232 |
. . . . 5
|
115 | 19, 37, 53, 70, 114 | en3d 7992 |
. . . 4
|
116 | 115 | exlimivv 1860 |
. . 3
|
117 | 3, 116 | sylbir 225 |
. 2
|
118 | 1, 2, 117 | syl2anb 496 |
1
|