Proof of Theorem mapsnd
Step | Hyp | Ref
| Expression |
1 | | mapsnd.1 |
. . . 4
|
2 | | mapsnd.2 |
. . . . 5
|
3 | | snex 4908 |
. . . . . 6
|
4 | 3 | a1i 11 |
. . . . 5
|
5 | 2, 4 | syl 17 |
. . . 4
|
6 | | elmapg 7870 |
. . . 4
|
7 | 1, 5, 6 | syl2anc 693 |
. . 3
|
8 | | ffn 6045 |
. . . . . . . . . . 11
|
9 | 8 | a1i 11 |
. . . . . . . . . 10
|
10 | 9 | imp 445 |
. . . . . . . . 9
|
11 | | snidg 4206 |
. . . . . . . . . . 11
|
12 | 2, 11 | syl 17 |
. . . . . . . . . 10
|
13 | 12 | adantr 481 |
. . . . . . . . 9
|
14 | | fneu 5995 |
. . . . . . . . 9
|
15 | 10, 13, 14 | syl2anc 693 |
. . . . . . . 8
|
16 | | euabsn 4261 |
. . . . . . . . . 10
|
17 | | frel 6050 |
. . . . . . . . . . . . . 14
|
18 | | relimasn 5488 |
. . . . . . . . . . . . . 14
|
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . 13
|
20 | | imadmrn 5476 |
. . . . . . . . . . . . . 14
|
21 | | fdm 6051 |
. . . . . . . . . . . . . . 15
|
22 | 21 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
|
23 | 20, 22 | syl5reqr 2671 |
. . . . . . . . . . . . 13
|
24 | 19, 23 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
25 | 24 | eqeq1d 2624 |
. . . . . . . . . . 11
|
26 | 25 | exbidv 1850 |
. . . . . . . . . 10
|
27 | 16, 26 | syl5bb 272 |
. . . . . . . . 9
|
28 | 27 | adantl 482 |
. . . . . . . 8
|
29 | 15, 28 | mpbid 222 |
. . . . . . 7
|
30 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
31 | 30 | snid 4208 |
. . . . . . . . . . . . . 14
|
32 | | eleq2 2690 |
. . . . . . . . . . . . . 14
|
33 | 31, 32 | mpbiri 248 |
. . . . . . . . . . . . 13
|
34 | | frn 6053 |
. . . . . . . . . . . . . 14
|
35 | 34 | sseld 3602 |
. . . . . . . . . . . . 13
|
36 | 33, 35 | syl5 34 |
. . . . . . . . . . . 12
|
37 | 36 | imp 445 |
. . . . . . . . . . 11
|
38 | 37 | adantll 750 |
. . . . . . . . . 10
|
39 | | dffn4 6121 |
. . . . . . . . . . . . . . . 16
|
40 | 8, 39 | sylib 208 |
. . . . . . . . . . . . . . 15
|
41 | | fof 6115 |
. . . . . . . . . . . . . . 15
|
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
|
43 | | feq3 6028 |
. . . . . . . . . . . . . 14
|
44 | 42, 43 | syl5ibcom 235 |
. . . . . . . . . . . . 13
|
45 | 44 | imp 445 |
. . . . . . . . . . . 12
|
46 | 45 | adantll 750 |
. . . . . . . . . . 11
|
47 | 2 | ad2antrr 762 |
. . . . . . . . . . . 12
|
48 | 30 | a1i 11 |
. . . . . . . . . . . 12
|
49 | | fsng 6404 |
. . . . . . . . . . . 12
|
50 | 47, 48, 49 | syl2anc 693 |
. . . . . . . . . . 11
|
51 | 46, 50 | mpbid 222 |
. . . . . . . . . 10
|
52 | 38, 51 | jca 554 |
. . . . . . . . 9
|
53 | 52 | ex 450 |
. . . . . . . 8
|
54 | 53 | eximdv 1846 |
. . . . . . 7
|
55 | 29, 54 | mpd 15 |
. . . . . 6
|
56 | | df-rex 2918 |
. . . . . 6
|
57 | 55, 56 | sylibr 224 |
. . . . 5
|
58 | 57 | ex 450 |
. . . 4
|
59 | 30 | a1i 11 |
. . . . . . . . . . . 12
|
60 | | f1osng 6177 |
. . . . . . . . . . . 12
|
61 | 2, 59, 60 | syl2anc 693 |
. . . . . . . . . . 11
|
62 | 61 | adantr 481 |
. . . . . . . . . 10
|
63 | | f1oeq1 6127 |
. . . . . . . . . . . 12
|
64 | 63 | bicomd 213 |
. . . . . . . . . . 11
|
65 | 64 | adantl 482 |
. . . . . . . . . 10
|
66 | 62, 65 | mpbid 222 |
. . . . . . . . 9
|
67 | | f1of 6137 |
. . . . . . . . 9
|
68 | 66, 67 | syl 17 |
. . . . . . . 8
|
69 | 68 | 3adant2 1080 |
. . . . . . 7
|
70 | | snssi 4339 |
. . . . . . . 8
|
71 | 70 | 3ad2ant2 1083 |
. . . . . . 7
|
72 | | fss 6056 |
. . . . . . 7
|
73 | 69, 71, 72 | syl2anc 693 |
. . . . . 6
|
74 | 73 | 3exp 1264 |
. . . . 5
|
75 | 74 | rexlimdv 3030 |
. . . 4
|
76 | 58, 75 | impbid 202 |
. . 3
|
77 | 7, 76 | bitrd 268 |
. 2
|
78 | 77 | abbi2dv 2742 |
1
|