Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(join‘𝐾) =
(join‘𝐾) |
2 | | eqid 2622 |
. . 3
⊢
(meet‘𝐾) =
(meet‘𝐾) |
3 | | eqid 2622 |
. . 3
⊢
(oc‘𝐾) =
(oc‘𝐾) |
4 | | docacl.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | docacl.t |
. . 3
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
6 | | docacl.i |
. . 3
⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
7 | | docacl.n |
. . 3
⊢ ⊥ =
((ocA‘𝐾)‘𝑊) |
8 | 1, 2, 3, 4, 5, 6, 7 | docavalN 36412 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ( ⊥ ‘𝑋) = (𝐼‘((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) |
9 | 4, 6 | diaf11N 36338 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→ran
𝐼) |
10 | | f1ofun 6139 |
. . . . 5
⊢ (𝐼:dom 𝐼–1-1-onto→ran
𝐼 → Fun 𝐼) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Fun 𝐼) |
12 | 11 | adantr 481 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → Fun 𝐼) |
13 | | hllat 34650 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
14 | 13 | ad2antrr 762 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → 𝐾 ∈ Lat) |
15 | | hlop 34649 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
16 | 15 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → 𝐾 ∈ OP) |
17 | | simpl 473 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
18 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ⊆ ran 𝐼 |
19 | 18 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ⊆ ran 𝐼) |
20 | 4, 5, 6 | dia1elN 36343 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑇 ∈ ran 𝐼) |
21 | 20 | anim1i 592 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (𝑇 ∈ ran 𝐼 ∧ 𝑋 ⊆ 𝑇)) |
22 | | sseq2 3627 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑇 → (𝑋 ⊆ 𝑧 ↔ 𝑋 ⊆ 𝑇)) |
23 | 22 | elrab 3363 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ↔ (𝑇 ∈ ran 𝐼 ∧ 𝑋 ⊆ 𝑇)) |
24 | 21, 23 | sylibr 224 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → 𝑇 ∈ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) |
25 | | ne0i 3921 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} → {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ≠ ∅) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ≠ ∅) |
27 | 4, 6 | diaintclN 36347 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ({𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ⊆ ran 𝐼 ∧ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ≠ ∅)) → ∩ {𝑧
∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ∈ ran 𝐼) |
28 | 17, 19, 26, 27 | syl12anc 1324 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ∈ ran 𝐼) |
29 | 4, 6 | diacnvclN 36340 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧} ∈ ran 𝐼) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) ∈ dom 𝐼) |
30 | 28, 29 | syldan 487 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) ∈ dom 𝐼) |
31 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝐾) =
(Base‘𝐾) |
32 | 31, 4, 6 | diadmclN 36326 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) ∈ dom 𝐼) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) ∈ (Base‘𝐾)) |
33 | 30, 32 | syldan 487 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) ∈ (Base‘𝐾)) |
34 | 31, 3 | opoccl 34481 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧})) ∈ (Base‘𝐾)) |
35 | 16, 33, 34 | syl2anc 693 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧})) ∈ (Base‘𝐾)) |
36 | 31, 4 | lhpbase 35284 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
37 | 36 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → 𝑊 ∈ (Base‘𝐾)) |
38 | 31, 3 | opoccl 34481 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) |
39 | 16, 37, 38 | syl2anc 693 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) |
40 | 31, 1 | latjcl 17051 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧})) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾)) |
41 | 14, 35, 39, 40 | syl3anc 1326 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾)) |
42 | 31, 2 | latmcl 17052 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧
(((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
43 | 14, 41, 37, 42 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
44 | | eqid 2622 |
. . . . . 6
⊢
(le‘𝐾) =
(le‘𝐾) |
45 | 31, 44, 2 | latmle2 17077 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧
(((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊) |
46 | 14, 41, 37, 45 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊) |
47 | 31, 44, 4, 6 | diaeldm 36325 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊))) |
48 | 47 | adantr 481 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊))) |
49 | 43, 46, 48 | mpbir2and 957 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼) |
50 | | fvelrn 6352 |
. . 3
⊢ ((Fun
𝐼 ∧ ((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ ran 𝐼) |
51 | 12, 49, 50 | syl2anc 693 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (𝐼‘((((oc‘𝐾)‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))(join‘𝐾)((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ ran 𝐼) |
52 | 8, 51 | eqeltrd 2701 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ( ⊥ ‘𝑋) ∈ ran 𝐼) |