Step | Hyp | Ref
| Expression |
1 | | xpcomf1o.1 |
. . . . . . . . . 10
|
2 | 1 | xpcomf1o 8049 |
. . . . . . . . 9
|
3 | | f1ofun 6139 |
. . . . . . . . 9
|
4 | | funbrfv2b 6240 |
. . . . . . . . 9
|
5 | 2, 3, 4 | mp2b 10 |
. . . . . . . 8
|
6 | | ancom 466 |
. . . . . . . 8
|
7 | | eqcom 2629 |
. . . . . . . . 9
|
8 | | f1odm 6141 |
. . . . . . . . . . 11
|
9 | 2, 8 | ax-mp 5 |
. . . . . . . . . 10
|
10 | 9 | eleq2i 2693 |
. . . . . . . . 9
|
11 | 7, 10 | anbi12i 733 |
. . . . . . . 8
|
12 | 5, 6, 11 | 3bitri 286 |
. . . . . . 7
|
13 | 12 | anbi1i 731 |
. . . . . 6
|
14 | | anass 681 |
. . . . . 6
|
15 | 13, 14 | bitri 264 |
. . . . 5
|
16 | 15 | exbii 1774 |
. . . 4
|
17 | | fvex 6201 |
. . . . 5
|
18 | | breq1 4656 |
. . . . . 6
|
19 | 18 | anbi2d 740 |
. . . . 5
|
20 | 17, 19 | ceqsexv 3242 |
. . . 4
|
21 | | elxp 5131 |
. . . . . 6
|
22 | 21 | anbi1i 731 |
. . . . 5
|
23 | | nfcv 2764 |
. . . . . . 7
|
24 | | xpcomco.1 |
. . . . . . . 8
|
25 | | nfmpt22 6723 |
. . . . . . . 8
|
26 | 24, 25 | nfcxfr 2762 |
. . . . . . 7
|
27 | | nfcv 2764 |
. . . . . . 7
|
28 | 23, 26, 27 | nfbr 4699 |
. . . . . 6
|
29 | 28 | 19.41 2103 |
. . . . 5
|
30 | | nfcv 2764 |
. . . . . . . . 9
|
31 | | nfmpt21 6722 |
. . . . . . . . . 10
|
32 | 24, 31 | nfcxfr 2762 |
. . . . . . . . 9
|
33 | | nfcv 2764 |
. . . . . . . . 9
|
34 | 30, 32, 33 | nfbr 4699 |
. . . . . . . 8
|
35 | 34 | 19.41 2103 |
. . . . . . 7
|
36 | | anass 681 |
. . . . . . . . 9
|
37 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
38 | | opelxpi 5148 |
. . . . . . . . . . . . . . 15
|
39 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 39 | cnveqd 5298 |
. . . . . . . . . . . . . . . . . 18
|
41 | 40 | unieqd 4446 |
. . . . . . . . . . . . . . . . 17
|
42 | | opswap 5622 |
. . . . . . . . . . . . . . . . 17
|
43 | 41, 42 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
44 | | opex 4932 |
. . . . . . . . . . . . . . . 16
|
45 | 43, 1, 44 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
|
46 | 38, 45 | syl 17 |
. . . . . . . . . . . . . 14
|
47 | 37, 46 | sylan9eq 2676 |
. . . . . . . . . . . . 13
|
48 | 47 | breq1d 4663 |
. . . . . . . . . . . 12
|
49 | | df-br 4654 |
. . . . . . . . . . . . . . . 16
|
50 | | df-mpt2 6655 |
. . . . . . . . . . . . . . . . . 18
|
51 | 24, 50 | eqtri 2644 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
|
53 | | oprabid 6677 |
. . . . . . . . . . . . . . . 16
|
54 | 49, 52, 53 | 3bitri 286 |
. . . . . . . . . . . . . . 15
|
55 | 54 | baib 944 |
. . . . . . . . . . . . . 14
|
56 | 55 | ancoms 469 |
. . . . . . . . . . . . 13
|
57 | 56 | adantl 482 |
. . . . . . . . . . . 12
|
58 | 48, 57 | bitrd 268 |
. . . . . . . . . . 11
|
59 | 58 | pm5.32da 673 |
. . . . . . . . . 10
|
60 | 59 | pm5.32i 669 |
. . . . . . . . 9
|
61 | 36, 60 | bitri 264 |
. . . . . . . 8
|
62 | 61 | exbii 1774 |
. . . . . . 7
|
63 | 35, 62 | bitr3i 266 |
. . . . . 6
|
64 | 63 | exbii 1774 |
. . . . 5
|
65 | 22, 29, 64 | 3bitr2i 288 |
. . . 4
|
66 | 16, 20, 65 | 3bitri 286 |
. . 3
|
67 | 66 | opabbii 4717 |
. 2
|
68 | | df-co 5123 |
. 2
|
69 | | df-mpt2 6655 |
. . 3
|
70 | | dfoprab2 6701 |
. . 3
|
71 | 69, 70 | eqtri 2644 |
. 2
|
72 | 67, 68, 71 | 3eqtr4i 2654 |
1
|