Step | Hyp | Ref
| Expression |
1 | | simpl2 1065 |
. . . 4
|
2 | | ssrab2 3687 |
. . . . 5
|
3 | | atlatmstc.b |
. . . . . . 7
|
4 | | atlatmstc.a |
. . . . . . 7
|
5 | 3, 4 | atssbase 34577 |
. . . . . 6
|
6 | | rabss2 3685 |
. . . . . 6
|
7 | 5, 6 | ax-mp 5 |
. . . . 5
|
8 | | atlatmstc.l |
. . . . . 6
|
9 | | atlatmstc.u |
. . . . . 6
|
10 | 3, 8, 9 | lubss 17121 |
. . . . 5
|
11 | 2, 7, 10 | mp3an23 1416 |
. . . 4
|
12 | 1, 11 | syl 17 |
. . 3
|
13 | | atlpos 34588 |
. . . . 5
|
14 | 13 | 3ad2ant3 1084 |
. . . 4
|
15 | | simpl 473 |
. . . . 5
|
16 | | simpr 477 |
. . . . 5
|
17 | 3, 8, 9, 15, 16 | lubid 16990 |
. . . 4
|
18 | 14, 17 | sylan 488 |
. . 3
|
19 | 12, 18 | breqtrd 4679 |
. 2
|
20 | | breq1 4656 |
. . . . . . . . . 10
|
21 | 20 | elrab 3363 |
. . . . . . . . 9
|
22 | | simpll2 1101 |
. . . . . . . . . . 11
|
23 | | ssrab2 3687 |
. . . . . . . . . . . . 13
|
24 | 23, 5 | sstri 3612 |
. . . . . . . . . . . 12
|
25 | 3, 8, 9 | lubel 17122 |
. . . . . . . . . . . 12
|
26 | 24, 25 | mp3an3 1413 |
. . . . . . . . . . 11
|
27 | 22, 26 | sylancom 701 |
. . . . . . . . . 10
|
28 | 27 | ex 450 |
. . . . . . . . 9
|
29 | 21, 28 | syl5bir 233 |
. . . . . . . 8
|
30 | 29 | expdimp 453 |
. . . . . . 7
|
31 | | simpll3 1102 |
. . . . . . . . . . 11
|
32 | | eqid 2622 |
. . . . . . . . . . . 12
|
33 | 32, 4 | atn0 34595 |
. . . . . . . . . . 11
|
34 | 31, 33 | sylancom 701 |
. . . . . . . . . 10
|
35 | 34 | adantr 481 |
. . . . . . . . 9
|
36 | | simpl3 1066 |
. . . . . . . . . . . . . . . 16
|
37 | | atllat 34587 |
. . . . . . . . . . . . . . . 16
|
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . 15
|
39 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
|
40 | 3, 4 | atbase 34576 |
. . . . . . . . . . . . . . 15
|
41 | 40 | adantl 482 |
. . . . . . . . . . . . . 14
|
42 | 3, 9 | clatlubcl 17112 |
. . . . . . . . . . . . . . . 16
|
43 | 1, 24, 42 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
44 | 43 | adantr 481 |
. . . . . . . . . . . . . 14
|
45 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
|
46 | | omlop 34528 |
. . . . . . . . . . . . . . . . 17
|
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
|
48 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
49 | 3, 48 | opoccl 34481 |
. . . . . . . . . . . . . . . 16
|
50 | 47, 43, 49 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
51 | 50 | adantr 481 |
. . . . . . . . . . . . . 14
|
52 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
53 | 3, 8, 52 | latlem12 17078 |
. . . . . . . . . . . . . 14
|
54 | 39, 41, 44, 51, 53 | syl13anc 1328 |
. . . . . . . . . . . . 13
|
55 | 3, 48, 52, 32 | opnoncon 34495 |
. . . . . . . . . . . . . . . 16
|
56 | 47, 43, 55 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
57 | 56 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
58 | 57 | adantr 481 |
. . . . . . . . . . . . 13
|
59 | 3, 8, 32 | ople0 34474 |
. . . . . . . . . . . . . 14
|
60 | 47, 40, 59 | syl2an 494 |
. . . . . . . . . . . . 13
|
61 | 54, 58, 60 | 3bitrd 294 |
. . . . . . . . . . . 12
|
62 | 61 | biimpa 501 |
. . . . . . . . . . 11
|
63 | 62 | expr 643 |
. . . . . . . . . 10
|
64 | 63 | necon3ad 2807 |
. . . . . . . . 9
|
65 | 35, 64 | mpd 15 |
. . . . . . . 8
|
66 | 65 | ex 450 |
. . . . . . 7
|
67 | 30, 66 | syld 47 |
. . . . . 6
|
68 | | imnan 438 |
. . . . . 6
|
69 | 67, 68 | sylib 208 |
. . . . 5
|
70 | | simplr 792 |
. . . . . 6
|
71 | 3, 8, 52 | latlem12 17078 |
. . . . . 6
|
72 | 39, 41, 70, 51, 71 | syl13anc 1328 |
. . . . 5
|
73 | 69, 72 | mtbid 314 |
. . . 4
|
74 | 73 | nrexdv 3001 |
. . 3
|
75 | | simpll3 1102 |
. . . . . 6
|
76 | | simpr 477 |
. . . . . . . 8
|
77 | 3, 52 | latmcl 17052 |
. . . . . . . 8
|
78 | 38, 76, 50, 77 | syl3anc 1326 |
. . . . . . 7
|
79 | 78 | adantr 481 |
. . . . . 6
|
80 | | simpr 477 |
. . . . . 6
|
81 | 3, 8, 32, 4 | atlex 34603 |
. . . . . 6
|
82 | 75, 79, 80, 81 | syl3anc 1326 |
. . . . 5
|
83 | 82 | ex 450 |
. . . 4
|
84 | 83 | necon1bd 2812 |
. . 3
|
85 | 74, 84 | mpd 15 |
. 2
|
86 | 3, 8, 52, 48, 32 | omllaw3 34532 |
. . 3
|
87 | 45, 43, 76, 86 | syl3anc 1326 |
. 2
|
88 | 19, 85, 87 | mp2and 715 |
1
|