Step | Hyp | Ref
| Expression |
1 | | relres 5426 |
. . 3
|
2 | 1 | a1i 11 |
. 2
|
3 | | dmfco 6272 |
. . . . . . . . 9
|
4 | 3 | biimpd 219 |
. . . . . . . 8
|
5 | 4 | funfni 5991 |
. . . . . . 7
|
6 | | dmressnsn 5438 |
. . . . . . . 8
|
7 | | eleq2 2690 |
. . . . . . . . . 10
|
8 | | velsn 4193 |
. . . . . . . . . . 11
|
9 | | dmressnsn 5438 |
. . . . . . . . . . . . . . . . 17
|
10 | | dffun7 5915 |
. . . . . . . . . . . . . . . . . . 19
|
11 | | snidg 4206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
12 | 11 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
13 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
14 | 13 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
16 | 12, 15 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
17 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
18 | 17 | isseti 3209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
19 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
20 | | fnbrfvb 6236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
21 | 19, 20 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
22 | 21 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
23 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
24 | 23 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
25 | 24 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
26 | 22, 25 | anim12ii 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
27 | 26 | eximdv 1846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
28 | 18, 27 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
29 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
30 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
31 | | brcog 5288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
32 | 29, 30, 31 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
34 | 28, 33 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
35 | | snidg 4206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
36 | 35 | biantrud 528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
37 | 30 | brres 5402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
38 | 36, 37 | syl6rbbr 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
39 | 38 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
40 | 34, 39 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
41 | 40 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
42 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
43 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
44 | 43 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
45 | 44 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
46 | 42, 45 | sylibd 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
47 | 46 | alrimiv 1855 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
48 | | moim 2519 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
50 | 49 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
51 | 50 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
52 | 16, 51 | rspcimdv 3310 |
. . . . . . . . . . . . . . . . . . . . . 22
|
53 | 52 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | 53 | com13 88 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 10, 55 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | com13 88 |
. . . . . . . . . . . . . . . . 17
|
58 | 9, 57 | mpcom 38 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | imp31 448 |
. . . . . . . . . . . . . . 15
|
60 | 17 | snid 4208 |
. . . . . . . . . . . . . . . . . 18
|
61 | 60 | biantru 526 |
. . . . . . . . . . . . . . . . 17
|
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
63 | 62 | mobidv 2491 |
. . . . . . . . . . . . . . 15
|
64 | 59, 63 | mpbid 222 |
. . . . . . . . . . . . . 14
|
65 | 64 | adantl 482 |
. . . . . . . . . . . . 13
|
66 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
|
67 | 30 | brres 5402 |
. . . . . . . . . . . . . . . 16
|
68 | 66, 67 | syl6rbb 277 |
. . . . . . . . . . . . . . 15
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . 14
|
70 | 69 | mobidv 2491 |
. . . . . . . . . . . . 13
|
71 | 65, 70 | mpbid 222 |
. . . . . . . . . . . 12
|
72 | 71 | ex 450 |
. . . . . . . . . . 11
|
73 | 8, 72 | sylbi 207 |
. . . . . . . . . 10
|
74 | 7, 73 | syl6bi 243 |
. . . . . . . . 9
|
75 | 74 | com23 86 |
. . . . . . . 8
|
76 | 6, 75 | syl 17 |
. . . . . . 7
|
77 | 5, 76 | syl6com 37 |
. . . . . 6
|
78 | 77 | a1d 25 |
. . . . 5
|
79 | 78 | imp31 448 |
. . . 4
|
80 | 79 | pm2.43i 52 |
. . 3
|
81 | 80 | ralrimiv 2965 |
. 2
|
82 | | dffun7 5915 |
. 2
|
83 | 2, 81, 82 | sylanbrc 698 |
1
|