Step | Hyp | Ref
| Expression |
1 | | diaintcl.h |
. . . . . . . 8
|
2 | | diaintcl.i |
. . . . . . . 8
|
3 | 1, 2 | diaf11N 36338 |
. . . . . . 7
|
4 | 3 | adantr 481 |
. . . . . 6
|
5 | | f1ofn 6138 |
. . . . . 6
|
6 | 4, 5 | syl 17 |
. . . . 5
|
7 | | cnvimass 5485 |
. . . . 5
|
8 | | fnssres 6004 |
. . . . 5
|
9 | 6, 7, 8 | sylancl 694 |
. . . 4
|
10 | | fniinfv 6257 |
. . . 4
|
11 | 9, 10 | syl 17 |
. . 3
|
12 | | df-ima 5127 |
. . . . 5
|
13 | | f1ofo 6144 |
. . . . . . . 8
|
14 | 3, 13 | syl 17 |
. . . . . . 7
|
15 | 14 | adantr 481 |
. . . . . 6
|
16 | | simprl 794 |
. . . . . 6
|
17 | | foimacnv 6154 |
. . . . . 6
|
18 | 15, 16, 17 | syl2anc 693 |
. . . . 5
|
19 | 12, 18 | syl5eqr 2670 |
. . . 4
|
20 | 19 | inteqd 4480 |
. . 3
|
21 | 11, 20 | eqtrd 2656 |
. 2
|
22 | | simpl 473 |
. . . . 5
|
23 | 7 | a1i 11 |
. . . . 5
|
24 | | simprr 796 |
. . . . . . 7
|
25 | | n0 3931 |
. . . . . . 7
|
26 | 24, 25 | sylib 208 |
. . . . . 6
|
27 | 16 | sselda 3603 |
. . . . . . . 8
|
28 | 3 | ad2antrr 762 |
. . . . . . . . . 10
|
29 | 28, 5 | syl 17 |
. . . . . . . . 9
|
30 | | fvelrnb 6243 |
. . . . . . . . 9
|
31 | 29, 30 | syl 17 |
. . . . . . . 8
|
32 | 27, 31 | mpbid 222 |
. . . . . . 7
|
33 | | f1ofun 6139 |
. . . . . . . . . . . . . . . 16
|
34 | 3, 33 | syl 17 |
. . . . . . . . . . . . . . 15
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . 14
|
36 | | fvimacnv 6332 |
. . . . . . . . . . . . . 14
|
37 | 35, 36 | sylan 488 |
. . . . . . . . . . . . 13
|
38 | | ne0i 3921 |
. . . . . . . . . . . . 13
|
39 | 37, 38 | syl6bi 243 |
. . . . . . . . . . . 12
|
40 | 39 | ex 450 |
. . . . . . . . . . 11
|
41 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
42 | 41 | biimprd 238 |
. . . . . . . . . . . 12
|
43 | 42 | imim1d 82 |
. . . . . . . . . . 11
|
44 | 40, 43 | syl9 77 |
. . . . . . . . . 10
|
45 | 44 | com24 95 |
. . . . . . . . 9
|
46 | 45 | imp 445 |
. . . . . . . 8
|
47 | 46 | rexlimdv 3030 |
. . . . . . 7
|
48 | 32, 47 | mpd 15 |
. . . . . 6
|
49 | 26, 48 | exlimddv 1863 |
. . . . 5
|
50 | | eqid 2622 |
. . . . . 6
|
51 | 50, 1, 2 | diaglbN 36344 |
. . . . 5
|
52 | 22, 23, 49, 51 | syl12anc 1324 |
. . . 4
|
53 | | fvres 6207 |
. . . . 5
|
54 | 53 | iineq2i 4540 |
. . . 4
|
55 | 52, 54 | syl6eqr 2674 |
. . 3
|
56 | | hlclat 34645 |
. . . . . . 7
|
57 | 56 | ad2antrr 762 |
. . . . . 6
|
58 | | eqid 2622 |
. . . . . . . . . 10
|
59 | | eqid 2622 |
. . . . . . . . . 10
|
60 | 58, 59, 1, 2 | diadm 36324 |
. . . . . . . . 9
|
61 | | ssrab2 3687 |
. . . . . . . . 9
|
62 | 60, 61 | syl6eqss 3655 |
. . . . . . . 8
|
63 | 62 | adantr 481 |
. . . . . . 7
|
64 | 7, 63 | syl5ss 3614 |
. . . . . 6
|
65 | 58, 50 | clatglbcl 17114 |
. . . . . 6
|
66 | 57, 64, 65 | syl2anc 693 |
. . . . 5
|
67 | | n0 3931 |
. . . . . . 7
|
68 | 49, 67 | sylib 208 |
. . . . . 6
|
69 | | hllat 34650 |
. . . . . . . 8
|
70 | 69 | ad3antrrr 766 |
. . . . . . 7
|
71 | 66 | adantr 481 |
. . . . . . 7
|
72 | 64 | sselda 3603 |
. . . . . . 7
|
73 | 58, 1 | lhpbase 35284 |
. . . . . . . 8
|
74 | 73 | ad3antlr 767 |
. . . . . . 7
|
75 | 56 | ad3antrrr 766 |
. . . . . . . 8
|
76 | 60 | adantr 481 |
. . . . . . . . . . 11
|
77 | 7, 76 | syl5sseq 3653 |
. . . . . . . . . 10
|
78 | 77, 61 | syl6ss 3615 |
. . . . . . . . 9
|
79 | 78 | adantr 481 |
. . . . . . . 8
|
80 | | simpr 477 |
. . . . . . . 8
|
81 | 58, 59, 50 | clatglble 17125 |
. . . . . . . 8
|
82 | 75, 79, 80, 81 | syl3anc 1326 |
. . . . . . 7
|
83 | 7 | sseli 3599 |
. . . . . . . . . 10
|
84 | 83 | adantl 482 |
. . . . . . . . 9
|
85 | 58, 59, 1, 2 | diaeldm 36325 |
. . . . . . . . . 10
|
86 | 85 | ad2antrr 762 |
. . . . . . . . 9
|
87 | 84, 86 | mpbid 222 |
. . . . . . . 8
|
88 | 87 | simprd 479 |
. . . . . . 7
|
89 | 58, 59, 70, 71, 72, 74, 82, 88 | lattrd 17058 |
. . . . . 6
|
90 | 68, 89 | exlimddv 1863 |
. . . . 5
|
91 | 58, 59, 1, 2 | diaeldm 36325 |
. . . . . 6
|
92 | 91 | adantr 481 |
. . . . 5
|
93 | 66, 90, 92 | mpbir2and 957 |
. . . 4
|
94 | 1, 2 | diaclN 36339 |
. . . 4
|
95 | 93, 94 | syldan 487 |
. . 3
|
96 | 55, 95 | eqeltrrd 2702 |
. 2
|
97 | 21, 96 | eqeltrrd 2702 |
1
|