Step Hyp Ref
Expression 1 bren 7545 . 2
2 bren 7545 . 2
3 eeanv 1988 . . 3
4 ovex 6324 . . . . . 6
5 4 a1i 11 . . . . 5
6 ovex 6324 . . . . . 6
7 6 a1i 11 . . . . 5
8 elmapi 7460 . . . . . . 7
9 f1of 5821 . . . . . . . . . . 11
10 9 adantr 465 . . . . . . . . . 10
11 fco 5746 . . . . . . . . . 10
12 10 , 11 sylan 471 . . . . . . . . 9
13 f1ocnv 5833 . . . . . . . . . . . 12
14 13 adantl 466 . . . . . . . . . . 11
15 f1of 5821 . . . . . . . . . . 11
16 14 , 15 syl 16 . . . . . . . . . 10
17 16 adantr 465 . . . . . . . . 9
18 fco 5746 . . . . . . . . 9
19 12 , 17 , 18 syl2anc 661 . . . . . . . 8
20 19 ex 434 . . . . . . 7
21 8 , 20 syl5 32 . . . . . 6
22 f1ofo 5828 . . . . . . . . . 10
23 22 adantr 465 . . . . . . . . 9
24 forn 5803 . . . . . . . . 9
25 23 , 24 syl 16 . . . . . . . 8
26 vex 3112 . . . . . . . . 9
27 26 rnex 6734 . . . . . . . 8
28 25 , 27 syl6eqelr 2554 . . . . . . 7
29 f1ofo 5828 . . . . . . . . . 10
30 29 adantl 466 . . . . . . . . 9
31 forn 5803 . . . . . . . . 9
32 30 , 31 syl 16 . . . . . . . 8
33 vex 3112 . . . . . . . . 9
34 33 rnex 6734 . . . . . . . 8
35 32 , 34 syl6eqelr 2554 . . . . . . 7
36 28 , 35 elmapd 7453 . . . . . 6
37 21 , 36 sylibrd 234 . . . . 5
38 elmapi 7460 . . . . . . 7
39 f1ocnv 5833 . . . . . . . . . . . 12
40 39 adantr 465 . . . . . . . . . . 11
41 f1of 5821 . . . . . . . . . . 11
42 40 , 41 syl 16 . . . . . . . . . 10
43 42 adantr 465 . . . . . . . . 9
44 id 22 . . . . . . . . . 10
45 f1of 5821 . . . . . . . . . . 11
46 45 adantl 466 . . . . . . . . . 10
47 fco 5746 . . . . . . . . . 10
48 44 , 46 , 47 syl2anr 478 . . . . . . . . 9
49 fco 5746 . . . . . . . . 9
50 43 , 48 , 49 syl2anc 661 . . . . . . . 8
51 50 ex 434 . . . . . . 7
52 38 , 51 syl5 32 . . . . . 6
53 f1odm 5825 . . . . . . . . 9
54 53 adantr 465 . . . . . . . 8
55 26 dmex 6733 . . . . . . . 8
56 54 , 55 syl6eqelr 2554 . . . . . . 7
57 f1odm 5825 . . . . . . . . 9
58 57 adantl 466 . . . . . . . 8
59 33 dmex 6733 . . . . . . . 8
60 58 , 59 syl6eqelr 2554 . . . . . . 7
61 56 , 60 elmapd 7453 . . . . . 6
62 52 , 61 sylibrd 234 . . . . 5
63 coass 5531 . . . . . . . . . . 11
64 f1ococnv2 5847 . . . . . . . . . . . . . 14
65 64 ad2antrr 725 . . . . . . . . . . . . 13
66 65 coeq1d 5169 . . . . . . . . . . . 12
67 48 adantrl 715 . . . . . . . . . . . . 13
68 fcoi2 5765 . . . . . . . . . . . . 13
69 67 , 68 syl 16 . . . . . . . . . . . 12
70 66 , 69 eqtrd 2498 . . . . . . . . . . 11
71 63 , 70 syl5eqr 2512 . . . . . . . . . 10
72 71 eqeq2d 2471 . . . . . . . . 9
73 coass 5531 . . . . . . . . . . . 12
74 f1ococnv1 5849 . . . . . . . . . . . . . . 15
75 74 ad2antlr 726 . . . . . . . . . . . . . 14
76 75 coeq2d 5170 . . . . . . . . . . . . 13
77 12 adantrr 716 . . . . . . . . . . . . . 14
78 fcoi1 5764 . . . . . . . . . . . . . 14
79 77 , 78 syl 16 . . . . . . . . . . . . 13
80 76 , 79 eqtrd 2498 . . . . . . . . . . . 12
81 73 , 80 syl5eq 2510 . . . . . . . . . . 11
82 81 eqeq2d 2471 . . . . . . . . . 10
83 eqcom 2466 . . . . . . . . . 10
84 82 , 83 syl6bb 261 . . . . . . . . 9
85 72 , 84 bitr4d 256 . . . . . . . 8
86 f1of1 5820 . . . . . . . . . 10
87 86 ad2antrr 725 . . . . . . . . 9
88 simprl 756 . . . . . . . . 9
89 50 adantrl 715 . . . . . . . . 9
90 cocan1 6194 . . . . . . . . 9
91 87 , 88 , 89 , 90 syl3anc 1228 . . . . . . . 8
92 30 adantr 465 . . . . . . . . 9
93 ffn 5736 . . . . . . . . . 10
94 93 ad2antll 728 . . . . . . . . 9
95 19 adantrr 716 . . . . . . . . . 10
96 ffn 5736 . . . . . . . . . 10
97 95 , 96 syl 16 . . . . . . . . 9
98 cocan2 6195 . . . . . . . . 9
99 92 , 94 , 97 , 98 syl3anc 1228 . . . . . . . 8
100 85 , 91 , 99 3bitr3d 283 . . . . . . 7
101 100 ex 434 . . . . . 6
102 8 , 38 , 101 syl2ani 656 . . . . 5
103 5 , 7 , 37 , 62 , 102 en3d 7572 . . . 4
104 103 exlimivv 1723 . . 3
105 3 , 104 sylbir 213 . 2
106 1 , 2 , 105 syl2anb 479 1
