Step | Hyp | Ref
| Expression |
1 | | df-rab 2921 |
. . 3
Scalar
Scalar |
2 | | relopab 5247 |
. . . . 5
|
3 | | diclspsn.l |
. . . . . . 7
|
4 | | diclspsn.a |
. . . . . . 7
|
5 | | diclspsn.h |
. . . . . . 7
|
6 | | diclspsn.p |
. . . . . . 7
|
7 | | diclspsn.t |
. . . . . . 7
|
8 | | eqid 2622 |
. . . . . . 7
|
9 | | diclspsn.i |
. . . . . . 7
|
10 | | diclspsn.f |
. . . . . . 7
|
11 | 3, 4, 5, 6, 7, 8, 9, 10 | dicval2 36468 |
. . . . . 6
|
12 | 11 | releqd 5203 |
. . . . 5
|
13 | 2, 12 | mpbiri 248 |
. . . 4
|
14 | | ssrab2 3687 |
. . . . . 6
Scalar |
15 | | relxp 5227 |
. . . . . 6
|
16 | | relss 5206 |
. . . . . 6
Scalar Scalar
|
17 | 14, 15, 16 | mp2 9 |
. . . . 5
Scalar |
18 | 17 | a1i 11 |
. . . 4
Scalar
|
19 | | id 22 |
. . . 4
|
20 | | vex 3203 |
. . . . . . 7
|
21 | | vex 3203 |
. . . . . . 7
|
22 | 3, 4, 5, 6, 7, 8, 9, 10, 20, 21 | dicopelval2 36470 |
. . . . . 6
|
23 | | simprl 794 |
. . . . . . . . . . 11
|
24 | | simpll 790 |
. . . . . . . . . . . 12
|
25 | | simprr 796 |
. . . . . . . . . . . 12
|
26 | | simpl 473 |
. . . . . . . . . . . . . 14
|
27 | 3, 4, 5, 6 | lhpocnel2 35305 |
. . . . . . . . . . . . . . 15
|
28 | 27 | adantr 481 |
. . . . . . . . . . . . . 14
|
29 | | simpr 477 |
. . . . . . . . . . . . . 14
|
30 | 3, 4, 5, 7, 10 | ltrniotacl 35867 |
. . . . . . . . . . . . . 14
|
31 | 26, 28, 29, 30 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
32 | 31 | adantr 481 |
. . . . . . . . . . . 12
|
33 | 5, 7, 8 | tendocl 36055 |
. . . . . . . . . . . 12
|
34 | 24, 25, 32, 33 | syl3anc 1326 |
. . . . . . . . . . 11
|
35 | 23, 34 | eqeltrd 2701 |
. . . . . . . . . 10
|
36 | 35, 25, 23 | 3jca 1242 |
. . . . . . . . 9
|
37 | | simpr3 1069 |
. . . . . . . . . 10
|
38 | | simpr2 1068 |
. . . . . . . . . 10
|
39 | 37, 38 | jca 554 |
. . . . . . . . 9
|
40 | 36, 39 | impbida 877 |
. . . . . . . 8
|
41 | | diclspsn.u |
. . . . . . . . . . . . . 14
|
42 | | eqid 2622 |
. . . . . . . . . . . . . 14
Scalar Scalar |
43 | | eqid 2622 |
. . . . . . . . . . . . . 14
Scalar Scalar |
44 | 5, 8, 41, 42, 43 | dvhbase 36372 |
. . . . . . . . . . . . 13
Scalar |
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
Scalar |
46 | 45 | rexeqdv 3145 |
. . . . . . . . . . 11
Scalar |
47 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
|
48 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
49 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
50 | 5, 7, 8 | tendoidcl 36057 |
. . . . . . . . . . . . . . . . . 18
|
51 | 50 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
52 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
53 | 5, 7, 8, 41, 52 | dvhopvsca 36391 |
. . . . . . . . . . . . . . . . 17
|
54 | 47, 48, 49, 51, 53 | syl13anc 1328 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
56 | 20, 21 | opth 4945 |
. . . . . . . . . . . . . . 15
|
57 | 55, 56 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
58 | 5, 7, 8 | tendo1mulr 36059 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
60 | 59 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
61 | | equcom 1945 |
. . . . . . . . . . . . . . . 16
|
62 | 60, 61 | syl6bb 276 |
. . . . . . . . . . . . . . 15
|
63 | 62 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
64 | 57, 63 | bitrd 268 |
. . . . . . . . . . . . 13
|
65 | | ancom 466 |
. . . . . . . . . . . . 13
|
66 | 64, 65 | syl6bb 276 |
. . . . . . . . . . . 12
|
67 | 66 | rexbidva 3049 |
. . . . . . . . . . 11
|
68 | 46, 67 | bitrd 268 |
. . . . . . . . . 10
Scalar |
69 | 68 | 3anbi3d 1405 |
. . . . . . . . 9
Scalar
|
70 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
71 | 70 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
72 | 71 | ceqsrexv 3336 |
. . . . . . . . . . . 12
|
73 | 72 | pm5.32i 669 |
. . . . . . . . . . 11
|
74 | 73 | anbi2i 730 |
. . . . . . . . . 10
|
75 | | 3anass 1042 |
. . . . . . . . . 10
|
76 | | 3anass 1042 |
. . . . . . . . . 10
|
77 | 74, 75, 76 | 3bitr4i 292 |
. . . . . . . . 9
|
78 | 69, 77 | syl6rbb 277 |
. . . . . . . 8
Scalar |
79 | 40, 78 | bitrd 268 |
. . . . . . 7
Scalar |
80 | | eqeq1 2626 |
. . . . . . . . . . 11
|
81 | 80 | rexbidv 3052 |
. . . . . . . . . 10
Scalar Scalar
|
82 | 81 | rabxp 5154 |
. . . . . . . . 9
Scalar
Scalar
|
83 | 82 | eleq2i 2693 |
. . . . . . . 8
Scalar
Scalar |
84 | | opabid 4982 |
. . . . . . . 8
Scalar
Scalar |
85 | 83, 84 | bitr2i 265 |
. . . . . . 7
Scalar
Scalar |
86 | 79, 85 | syl6bb 276 |
. . . . . 6
Scalar
|
87 | 22, 86 | bitrd 268 |
. . . . 5
Scalar |
88 | 87 | eqrelrdv2 5219 |
. . . 4
Scalar
Scalar |
89 | 13, 18, 19, 88 | syl21anc 1325 |
. . 3
Scalar |
90 | | simpll 790 |
. . . . . . . 8
Scalar |
91 | 45 | eleq2d 2687 |
. . . . . . . . 9
Scalar
|
92 | 91 | biimpa 501 |
. . . . . . . 8
Scalar |
93 | 50 | adantr 481 |
. . . . . . . . . 10
|
94 | | opelxpi 5148 |
. . . . . . . . . 10
|
95 | 31, 93, 94 | syl2anc 693 |
. . . . . . . . 9
|
96 | 95 | adantr 481 |
. . . . . . . 8
Scalar
|
97 | 5, 7, 8, 41, 52 | dvhvscacl 36392 |
. . . . . . . 8
|
98 | 90, 92, 96, 97 | syl12anc 1324 |
. . . . . . 7
Scalar |
99 | | eleq1a 2696 |
. . . . . . 7
|
100 | 98, 99 | syl 17 |
. . . . . 6
Scalar
|
101 | 100 | rexlimdva 3031 |
. . . . 5
Scalar |
102 | 101 | pm4.71rd 667 |
. . . 4
Scalar
Scalar |
103 | 102 | abbidv 2741 |
. . 3
Scalar
Scalar |
104 | 1, 89, 103 | 3eqtr4a 2682 |
. 2
Scalar |
105 | 5, 41, 26 | dvhlmod 36399 |
. . 3
|
106 | | eqid 2622 |
. . . . 5
|
107 | 5, 7, 8, 41, 106 | dvhelvbasei 36377 |
. . . 4
|
108 | 26, 31, 93, 107 | syl12anc 1324 |
. . 3
|
109 | | diclspsn.n |
. . . 4
|
110 | 42, 43, 106, 52, 109 | lspsn 19002 |
. . 3
Scalar |
111 | 105, 108,
110 | syl2anc 693 |
. 2
Scalar
|
112 | 104, 111 | eqtr4d 2659 |
1
|