Step | Hyp | Ref
| Expression |
1 | | df-rel 5121 |
. 2
|
2 | | dfss2 3591 |
. . . . 5
|
3 | | relop.1 |
. . . . . . . . . 10
|
4 | | relop.2 |
. . . . . . . . . 10
|
5 | 3, 4 | elop 4935 |
. . . . . . . . 9
|
6 | | elvv 5177 |
. . . . . . . . 9
|
7 | 5, 6 | imbi12i 340 |
. . . . . . . 8
|
8 | | jaob 822 |
. . . . . . . 8
|
9 | 7, 8 | bitri 264 |
. . . . . . 7
|
10 | 9 | albii 1747 |
. . . . . 6
|
11 | | 19.26 1798 |
. . . . . 6
|
12 | 10, 11 | bitri 264 |
. . . . 5
|
13 | 2, 12 | bitri 264 |
. . . 4
|
14 | | snex 4908 |
. . . . . . 7
|
15 | | eqeq1 2626 |
. . . . . . . 8
|
16 | | eqeq1 2626 |
. . . . . . . . . 10
|
17 | | eqcom 2629 |
. . . . . . . . . . 11
|
18 | | vex 3203 |
. . . . . . . . . . . 12
|
19 | | vex 3203 |
. . . . . . . . . . . 12
|
20 | 18, 19, 3 | opeqsn 4967 |
. . . . . . . . . . 11
|
21 | 17, 20 | bitri 264 |
. . . . . . . . . 10
|
22 | 16, 21 | syl6bb 276 |
. . . . . . . . 9
|
23 | 22 | 2exbidv 1852 |
. . . . . . . 8
|
24 | 15, 23 | imbi12d 334 |
. . . . . . 7
|
25 | 14, 24 | spcv 3299 |
. . . . . 6
|
26 | | sneq 4187 |
. . . . . . . . 9
|
27 | 26 | eqeq2d 2632 |
. . . . . . . 8
|
28 | 27 | cbvexv 2275 |
. . . . . . 7
|
29 | | ax6evr 1942 |
. . . . . . . . 9
|
30 | | 19.41v 1914 |
. . . . . . . . 9
|
31 | 29, 30 | mpbiran 953 |
. . . . . . . 8
|
32 | 31 | exbii 1774 |
. . . . . . 7
|
33 | | eqid 2622 |
. . . . . . . 8
|
34 | 33 | a1bi 352 |
. . . . . . 7
|
35 | 28, 32, 34 | 3bitr2ri 289 |
. . . . . 6
|
36 | 25, 35 | sylib 208 |
. . . . 5
|
37 | | eqid 2622 |
. . . . . 6
|
38 | | prex 4909 |
. . . . . . 7
|
39 | | eqeq1 2626 |
. . . . . . . 8
|
40 | | eqeq1 2626 |
. . . . . . . . 9
|
41 | 40 | 2exbidv 1852 |
. . . . . . . 8
|
42 | 39, 41 | imbi12d 334 |
. . . . . . 7
|
43 | 38, 42 | spcv 3299 |
. . . . . 6
|
44 | 37, 43 | mpi 20 |
. . . . 5
|
45 | | eqcom 2629 |
. . . . . . . . . 10
|
46 | 18, 19, 3, 4 | opeqpr 4968 |
. . . . . . . . . 10
|
47 | 45, 46 | bitri 264 |
. . . . . . . . 9
|
48 | | idd 24 |
. . . . . . . . . 10
|
49 | | eqtr2 2642 |
. . . . . . . . . . . . . 14
|
50 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
51 | 18, 19, 50 | preqsn 4393 |
. . . . . . . . . . . . . . 15
|
52 | 51 | simplbi 476 |
. . . . . . . . . . . . . 14
|
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . 13
|
54 | | dfsn2 4190 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . . 20
|
56 | 54, 55 | syl5req 2669 |
. . . . . . . . . . . . . . . . . . 19
|
57 | 56 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
58 | 54, 55 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 58 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
60 | 57, 59 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
61 | 60 | biimpd 219 |
. . . . . . . . . . . . . . . 16
|
62 | 61 | expd 452 |
. . . . . . . . . . . . . . 15
|
63 | 62 | com12 32 |
. . . . . . . . . . . . . 14
|
64 | 63 | adantr 481 |
. . . . . . . . . . . . 13
|
65 | 53, 64 | mpd 15 |
. . . . . . . . . . . 12
|
66 | 65 | expcom 451 |
. . . . . . . . . . 11
|
67 | 66 | impd 447 |
. . . . . . . . . 10
|
68 | 48, 67 | jaod 395 |
. . . . . . . . 9
|
69 | 47, 68 | syl5bi 232 |
. . . . . . . 8
|
70 | 69 | 2eximdv 1848 |
. . . . . . 7
|
71 | 70 | exlimiv 1858 |
. . . . . 6
|
72 | 71 | imp 445 |
. . . . 5
|
73 | 36, 44, 72 | syl2an 494 |
. . . 4
|
74 | 13, 73 | sylbi 207 |
. . 3
|
75 | | simpr 477 |
. . . . . . . . . . 11
|
76 | | equid 1939 |
. . . . . . . . . . . . . 14
|
77 | 76 | jctl 564 |
. . . . . . . . . . . . 13
|
78 | 18, 18, 3 | opeqsn 4967 |
. . . . . . . . . . . . 13
|
79 | 77, 78 | sylibr 224 |
. . . . . . . . . . . 12
|
80 | 79 | adantr 481 |
. . . . . . . . . . 11
|
81 | 75, 80 | eqtr4d 2659 |
. . . . . . . . . 10
|
82 | | opeq12 4404 |
. . . . . . . . . . . 12
|
83 | 82 | eqeq2d 2632 |
. . . . . . . . . . 11
|
84 | 18, 18, 83 | spc2ev 3301 |
. . . . . . . . . 10
|
85 | 81, 84 | syl 17 |
. . . . . . . . 9
|
86 | 85 | adantlr 751 |
. . . . . . . 8
|
87 | | preq12 4270 |
. . . . . . . . . . . 12
|
88 | 87 | eqeq2d 2632 |
. . . . . . . . . . 11
|
89 | 88 | biimpa 501 |
. . . . . . . . . 10
|
90 | 18, 19 | dfop 4401 |
. . . . . . . . . 10
|
91 | 89, 90 | syl6eqr 2674 |
. . . . . . . . 9
|
92 | | opeq12 4404 |
. . . . . . . . . . 11
|
93 | 92 | eqeq2d 2632 |
. . . . . . . . . 10
|
94 | 18, 19, 93 | spc2ev 3301 |
. . . . . . . . 9
|
95 | 91, 94 | syl 17 |
. . . . . . . 8
|
96 | 86, 95 | jaodan 826 |
. . . . . . 7
|
97 | 96 | ex 450 |
. . . . . 6
|
98 | | elvv 5177 |
. . . . . 6
|
99 | 97, 5, 98 | 3imtr4g 285 |
. . . . 5
|
100 | 99 | ssrdv 3609 |
. . . 4
|
101 | 100 | exlimivv 1860 |
. . 3
|
102 | 74, 101 | impbii 199 |
. 2
|
103 | 1, 102 | bitri 264 |
1
|