Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
|
2 | | eqid 2622 |
. . 3
|
3 | | eqid 2622 |
. . 3
|
4 | | eqid 2622 |
. . 3
|
5 | 1, 2, 3, 4 | hlhgt4 34674 |
. 2
|
6 | | simpl1 1064 |
. . . . . . . . 9
|
7 | | hlop 34649 |
. . . . . . . . . 10
|
8 | 1, 3 | op0cl 34471 |
. . . . . . . . . 10
|
9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . 9
|
10 | | simpl2l 1114 |
. . . . . . . . 9
|
11 | | simprll 802 |
. . . . . . . . 9
|
12 | | eqid 2622 |
. . . . . . . . . 10
|
13 | | athgt.j |
. . . . . . . . . 10
|
14 | | athgt.c |
. . . . . . . . . 10
|
15 | | athgt.a |
. . . . . . . . . 10
|
16 | 1, 12, 2, 13, 14, 15 | hlrelat3 34698 |
. . . . . . . . 9
|
17 | 6, 9, 10, 11, 16 | syl31anc 1329 |
. . . . . . . 8
|
18 | | simp11 1091 |
. . . . . . . . . . . . . 14
|
19 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
20 | 3, 14, 15 | atcvr0 34575 |
. . . . . . . . . . . . . 14
|
21 | 18, 19, 20 | syl2anc 693 |
. . . . . . . . . . . . 13
|
22 | | hlol 34648 |
. . . . . . . . . . . . . . 15
|
23 | 18, 22 | syl 17 |
. . . . . . . . . . . . . 14
|
24 | 1, 15 | atbase 34576 |
. . . . . . . . . . . . . . 15
|
25 | 24 | 3ad2ant3 1084 |
. . . . . . . . . . . . . 14
|
26 | 1, 13, 3 | olj02 34513 |
. . . . . . . . . . . . . 14
|
27 | 23, 25, 26 | syl2anc 693 |
. . . . . . . . . . . . 13
|
28 | 21, 27 | breqtrrd 4681 |
. . . . . . . . . . . 12
|
29 | 28 | biantrurd 529 |
. . . . . . . . . . 11
|
30 | 27 | breq1d 4663 |
. . . . . . . . . . 11
|
31 | 29, 30 | bitr3d 270 |
. . . . . . . . . 10
|
32 | 31 | 3expa 1265 |
. . . . . . . . 9
|
33 | 32 | rexbidva 3049 |
. . . . . . . 8
|
34 | 17, 33 | mpbid 222 |
. . . . . . 7
|
35 | | simp11 1091 |
. . . . . . . . . . . 12
|
36 | 25 | 3adant3r 1323 |
. . . . . . . . . . . 12
|
37 | | simp12r 1175 |
. . . . . . . . . . . 12
|
38 | | simp3r 1090 |
. . . . . . . . . . . . 13
|
39 | | simp2lr 1129 |
. . . . . . . . . . . . 13
|
40 | | hlpos 34652 |
. . . . . . . . . . . . . . 15
|
41 | 35, 40 | syl 17 |
. . . . . . . . . . . . . 14
|
42 | | simp12l 1174 |
. . . . . . . . . . . . . 14
|
43 | 1, 12, 2 | plelttr 16972 |
. . . . . . . . . . . . . 14
|
44 | 41, 36, 42, 37, 43 | syl13anc 1328 |
. . . . . . . . . . . . 13
|
45 | 38, 39, 44 | mp2and 715 |
. . . . . . . . . . . 12
|
46 | 1, 12, 2, 13, 14, 15 | hlrelat3 34698 |
. . . . . . . . . . . 12
|
47 | 35, 36, 37, 45, 46 | syl31anc 1329 |
. . . . . . . . . . 11
|
48 | | simp11 1091 |
. . . . . . . . . . . . . . . . . . . . . 22
|
49 | | hllat 34650 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | | simp3ll 1132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
52 | 51, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | | simp3lr 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
54 | 1, 15 | atbase 34576 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
56 | 1, 13 | latjcl 17051 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
57 | 50, 52, 55, 56 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
|
58 | | simp13 1093 |
. . . . . . . . . . . . . . . . . . . . . 22
|
59 | | simp3r 1090 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
60 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
61 | 48, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
62 | | simp12 1092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
63 | 1, 12, 2 | plelttr 16972 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
64 | 61, 57, 62, 58, 63 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 59, 60, 64 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | 1, 12, 2, 13, 14, 15 | hlrelat3 34698 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 48, 57, 58, 65, 66 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | | simp1ll 1124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
69 | 68, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
70 | | simp2ll 1128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
71 | 70, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
72 | | simp2lr 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
73 | 72, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
74 | 69, 71, 73, 56 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
75 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
76 | 1, 15 | atbase 34576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
78 | 1, 13 | latjcl 17051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
79 | 69, 74, 77, 78 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
80 | 1, 4 | op1cl 34472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
81 | 68, 7, 80 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
82 | | simp3r 1090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
83 | | simp1r 1086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
84 | 68, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
85 | | simp1lr 1125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
86 | 1, 12, 2 | plelttr 16972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
87 | 84, 79, 85, 81, 86 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
88 | 82, 83, 87 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
89 | 1, 12, 2, 13, 14, 15 | hlrelat3 34698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
90 | 68, 79, 81, 88, 89 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
91 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
92 | 91 | reximi 3011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
93 | 90, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
94 | 93 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
95 | 94 | exp4a 633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
96 | 95 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
97 | 96 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
98 | 97 | 3imp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
99 | 98 | 3adant2l 1320 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
100 | 99 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 100 | anim2d 589 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 101 | reximdva 3017 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | 67, 102 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | 103 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 104 | exp4a 633 |
. . . . . . . . . . . . . . . . . 18
|
106 | 105 | exp4a 633 |
. . . . . . . . . . . . . . . . 17
|
107 | 106 | 3adant2l 1320 |
. . . . . . . . . . . . . . . 16
|
108 | 107 | 3imp1 1280 |
. . . . . . . . . . . . . . 15
|
109 | 108 | anim2d 589 |
. . . . . . . . . . . . . 14
|
110 | 109 | reximdva 3017 |
. . . . . . . . . . . . 13
|
111 | 110 | 3adant2l 1320 |
. . . . . . . . . . . 12
|
112 | 111 | 3adant3r 1323 |
. . . . . . . . . . 11
|
113 | 47, 112 | mpd 15 |
. . . . . . . . . 10
|
114 | 113 | 3expia 1267 |
. . . . . . . . 9
|
115 | 114 | expd 452 |
. . . . . . . 8
|
116 | 115 | reximdvai 3015 |
. . . . . . 7
|
117 | 34, 116 | mpd 15 |
. . . . . 6
|
118 | 117 | 3exp1 1283 |
. . . . 5
|
119 | 118 | imp 445 |
. . . 4
|
120 | 119 | rexlimdv 3030 |
. . 3
|
121 | 120 | rexlimdvva 3038 |
. 2
|
122 | 5, 121 | mpd 15 |
1
|