Step Hyp Ref
Expression 1 axcc3.2 . . 3
2 relen 7541 . . . 4
3 2 brrelexi 5045 . . 3
4 mptexg 6142 . . 3
5 1 , 3 , 4 mp2b 10 . 2
6 bren 7545 . . . 4
7 1 , 6 mpbi 208 . . 3
8 axcc2 8838 . . . . 5
9 f1of 5821 . . . . . . . . . . 11
10 fnfco 5755 . . . . . . . . . . 11
11 9 , 10 sylan2 474 . . . . . . . . . 10
12 11 adantlr 714 . . . . . . . . 9
13 12 3adant1 1014 . . . . . . . 8
14 nfmpt1 4541 . . . . . . . . . . 11
15 14 nfeq2 2636 . . . . . . . . . 10
16 nfv 1707 . . . . . . . . . 10
17 nfv 1707 . . . . . . . . . 10
18 15 , 16 , 17 nf3an 1930 . . . . . . . . 9
19 9 ffvelrnda 6031 . . . . . . . . . . . . . . . . . 18
20 fveq2 5871 . . . . . . . . . . . . . . . . . . . . 21
21 20 neeq1d 2734 . . . . . . . . . . . . . . . . . . . 20
22 fveq2 5871 . . . . . . . . . . . . . . . . . . . . 21
23 22 , 20 eleq12d 2539 . . . . . . . . . . . . . . . . . . . 20
24 21 , 23 imbi12d 320 . . . . . . . . . . . . . . . . . . 19
25 24 rspcv 3206 . . . . . . . . . . . . . . . . . 18
26 19 , 25 syl 16 . . . . . . . . . . . . . . . . 17
27 26 3ad2antl3 1160 . . . . . . . . . . . . . . . 16
28 f1ocnv 5833 . . . . . . . . . . . . . . . . . . . . . . . . 25
29 f1of 5821 . . . . . . . . . . . . . . . . . . . . . . . . 25
30 28 , 29 syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
31 fvco3 5950 . . . . . . . . . . . . . . . . . . . . . . . 24
32 30 , 31 sylan 471 . . . . . . . . . . . . . . . . . . . . . . 23
33 19 , 32 syldan 470 . . . . . . . . . . . . . . . . . . . . . 22
34 33 3adant1 1014 . . . . . . . . . . . . . . . . . . . . 21
35 f1ocnvfv1 6182 . . . . . . . . . . . . . . . . . . . . . . 23
36 35 fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . 22
37 36 3adant1 1014 . . . . . . . . . . . . . . . . . . . . 21
38 fveq1 5870 . . . . . . . . . . . . . . . . . . . . . . 23
39 axcc3.1 . . . . . . . . . . . . . . . . . . . . . . . 24
40 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . 25
41 40 fvmpt2 5963 . . . . . . . . . . . . . . . . . . . . . . . 24
42 39 , 41 mpan2 671 . . . . . . . . . . . . . . . . . . . . . . 23
43 38 , 42 sylan9eq 2518 . . . . . . . . . . . . . . . . . . . . . 22
44 43 3adant2 1015 . . . . . . . . . . . . . . . . . . . . 21
45 34 , 37 , 44 3eqtrd 2502 . . . . . . . . . . . . . . . . . . . 20
46 45 3expa 1196 . . . . . . . . . . . . . . . . . . 19
47 46 3adantl2 1153 . . . . . . . . . . . . . . . . . 18
48 47 neeq1d 2734 . . . . . . . . . . . . . . . . 17
49 9 3ad2ant3 1019 . . . . . . . . . . . . . . . . . . . 20
50 fvco3 5950 . . . . . . . . . . . . . . . . . . . 20
51 49 , 50 sylan 471 . . . . . . . . . . . . . . . . . . 19
52 51 eleq1d 2526 . . . . . . . . . . . . . . . . . 18
53 47 eleq2d 2527 . . . . . . . . . . . . . . . . . 18
54 52 , 53 bitr3d 255 . . . . . . . . . . . . . . . . 17
55 48 , 54 imbi12d 320 . . . . . . . . . . . . . . . 16
56 27 , 55 sylibd 214 . . . . . . . . . . . . . . 15
57 56 ex 434 . . . . . . . . . . . . . 14
58 57 com23 78 . . . . . . . . . . . . 13
59 58 3exp 1195 . . . . . . . . . . . 12
60 59 com34 83 . . . . . . . . . . 11
61 60 imp32 433 . . . . . . . . . 10
62 61 3impia 1193 . . . . . . . . 9
63 18 , 62 ralrimi 2857 . . . . . . . 8
64 vex 3112 . . . . . . . . . 10
65 vex 3112 . . . . . . . . . 10
66 64 , 65 coex 6752 . . . . . . . . 9
67 fneq1 5674 . . . . . . . . . 10
68 fveq1 5870 . . . . . . . . . . . . 13
69 68 eleq1d 2526 . . . . . . . . . . . 12
70 69 imbi2d 316 . . . . . . . . . . 11
71 70 ralbidv 2896 . . . . . . . . . 10
72 67 , 71 anbi12d 710 . . . . . . . . 9
73 66 , 72 spcev 3201 . . . . . . . 8
74 13 , 63 , 73 syl2anc 661 . . . . . . 7
75 74 3exp 1195 . . . . . 6
76 75 exlimdv 1724 . . . . 5
77 8 , 76 mpi 17 . . . 4
78 77 exlimdv 1724 . . 3
79 7 , 78 mpi 17 . 2
80 5 , 79 vtocle 3183 1
