Step | Hyp | Ref
| Expression |
1 | | dihglblem6.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
2 | | dihglblem6.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | eqid 2740 |
. . . 4
⊢
(meet‘𝐾) =
(meet‘𝐾) |
4 | | dihglblem6.g |
. . . 4
⊢ 𝐺 = (glb‘𝐾) |
5 | | dihglblem6.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | eqid 2740 |
. . . 4
⊢ {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣(meet‘𝐾)𝑊)} = {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣(meet‘𝐾)𝑊)} |
7 | | eqid 2740 |
. . . 4
⊢
((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊) |
8 | | dihglblem6.i |
. . . 4
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | dihglblem4 39320 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) |
10 | | fal 1556 |
. . . . 5
⊢ ¬
⊥ |
11 | | dihglblem6.s |
. . . . . . . 8
⊢ 𝑃 = (LSubSp‘𝑈) |
12 | | dihglblem6.d |
. . . . . . . 8
⊢ 𝐷 = (LSAtoms‘𝑈) |
13 | | dihglblem6.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
14 | | simpll 764 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
15 | 5, 13, 14 | dvhlmod 39133 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → 𝑈 ∈ LMod) |
16 | | simplll 772 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → 𝐾 ∈ HL) |
17 | | hlclat 37381 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → 𝐾 ∈ CLat) |
19 | | simplrl 774 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → 𝑆 ⊆ 𝐵) |
20 | 1, 4 | clatglbcl 18234 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) |
21 | 18, 19, 20 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → (𝐺‘𝑆) ∈ 𝐵) |
22 | 1, 5, 8, 13, 11 | dihlss 39273 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺‘𝑆) ∈ 𝐵) → (𝐼‘(𝐺‘𝑆)) ∈ 𝑃) |
23 | 14, 21, 22 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → (𝐼‘(𝐺‘𝑆)) ∈ 𝑃) |
24 | 1, 4, 5, 13, 8, 11 | dihglblem5 39321 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑃) |
25 | 24 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑃) |
26 | | simpr 485 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) |
27 | 11, 12, 15, 23, 25, 26 | lpssat 37036 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) → ∃𝑝 ∈ 𝐷 (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) |
28 | 27 | ex 413 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → ((𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) → ∃𝑝 ∈ 𝐷 (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆))))) |
29 | | simp1l 1196 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
30 | 5, 13, 8, 12 | dih1dimat 39353 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ 𝐷) → 𝑝 ∈ ran 𝐼) |
31 | 30 | adantlr 712 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) → 𝑝 ∈ ran 𝐼) |
32 | 31 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → 𝑝 ∈ ran 𝐼) |
33 | 5, 8 | dihcnvid2 39296 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ ran 𝐼) → (𝐼‘(◡𝐼‘𝑝)) = 𝑝) |
34 | 29, 32, 33 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → (𝐼‘(◡𝐼‘𝑝)) = 𝑝) |
35 | | simp3l 1200 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → 𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥)) |
36 | | ssiin 4990 |
. . . . . . . . . . . . 13
⊢ (𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 𝑝 ⊆ (𝐼‘𝑥)) |
37 | 35, 36 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → ∀𝑥 ∈ 𝑆 𝑝 ⊆ (𝐼‘𝑥)) |
38 | | simplll 772 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
39 | | simpll 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
40 | 1, 5, 8, 13, 11 | dihf11 39290 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:𝐵–1-1→𝑃) |
41 | | f1f1orn 6725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼:𝐵–1-1→𝑃 → 𝐼:𝐵–1-1-onto→ran
𝐼) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) → 𝐼:𝐵–1-1-onto→ran
𝐼) |
43 | | f1ocnvdm 7154 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼:𝐵–1-1-onto→ran
𝐼 ∧ 𝑝 ∈ ran 𝐼) → (◡𝐼‘𝑝) ∈ 𝐵) |
44 | 42, 31, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) → (◡𝐼‘𝑝) ∈ 𝐵) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → (◡𝐼‘𝑝) ∈ 𝐵) |
46 | | simplrl 774 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) → 𝑆 ⊆ 𝐵) |
47 | 46 | sselda 3926 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
48 | 1, 2, 5, 8 | dihord 39287 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (◡𝐼‘𝑝) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → ((𝐼‘(◡𝐼‘𝑝)) ⊆ (𝐼‘𝑥) ↔ (◡𝐼‘𝑝) ≤ 𝑥)) |
49 | 38, 45, 47, 48 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → ((𝐼‘(◡𝐼‘𝑝)) ⊆ (𝐼‘𝑥) ↔ (◡𝐼‘𝑝) ≤ 𝑥)) |
50 | 39, 31, 33 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) → (𝐼‘(◡𝐼‘𝑝)) = 𝑝) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → (𝐼‘(◡𝐼‘𝑝)) = 𝑝) |
52 | 51 | sseq1d 3957 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → ((𝐼‘(◡𝐼‘𝑝)) ⊆ (𝐼‘𝑥) ↔ 𝑝 ⊆ (𝐼‘𝑥))) |
53 | 49, 52 | bitr3d 280 |
. . . . . . . . . . . . . 14
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → ((◡𝐼‘𝑝) ≤ 𝑥 ↔ 𝑝 ⊆ (𝐼‘𝑥))) |
54 | 53 | ralbidva 3122 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷) → (∀𝑥 ∈ 𝑆 (◡𝐼‘𝑝) ≤ 𝑥 ↔ ∀𝑥 ∈ 𝑆 𝑝 ⊆ (𝐼‘𝑥))) |
55 | 54 | 3adant3 1131 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → (∀𝑥 ∈ 𝑆 (◡𝐼‘𝑝) ≤ 𝑥 ↔ ∀𝑥 ∈ 𝑆 𝑝 ⊆ (𝐼‘𝑥))) |
56 | 37, 55 | mpbird 256 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → ∀𝑥 ∈ 𝑆 (◡𝐼‘𝑝) ≤ 𝑥) |
57 | | simp1ll 1235 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → 𝐾 ∈ HL) |
58 | 57, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → 𝐾 ∈ CLat) |
59 | 44 | 3adant3 1131 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → (◡𝐼‘𝑝) ∈ 𝐵) |
60 | | simp1rl 1237 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → 𝑆 ⊆ 𝐵) |
61 | 1, 2, 4 | clatleglb 18247 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ CLat ∧ (◡𝐼‘𝑝) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → ((◡𝐼‘𝑝) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (◡𝐼‘𝑝) ≤ 𝑥)) |
62 | 58, 59, 60, 61 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → ((◡𝐼‘𝑝) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (◡𝐼‘𝑝) ≤ 𝑥)) |
63 | 56, 62 | mpbird 256 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → (◡𝐼‘𝑝) ≤ (𝐺‘𝑆)) |
64 | 58, 60, 20 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → (𝐺‘𝑆) ∈ 𝐵) |
65 | 1, 2, 5, 8 | dihord 39287 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (◡𝐼‘𝑝) ∈ 𝐵 ∧ (𝐺‘𝑆) ∈ 𝐵) → ((𝐼‘(◡𝐼‘𝑝)) ⊆ (𝐼‘(𝐺‘𝑆)) ↔ (◡𝐼‘𝑝) ≤ (𝐺‘𝑆))) |
66 | 29, 59, 64, 65 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → ((𝐼‘(◡𝐼‘𝑝)) ⊆ (𝐼‘(𝐺‘𝑆)) ↔ (◡𝐼‘𝑝) ≤ (𝐺‘𝑆))) |
67 | 63, 66 | mpbird 256 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → (𝐼‘(◡𝐼‘𝑝)) ⊆ (𝐼‘(𝐺‘𝑆))) |
68 | 34, 67 | eqsstrrd 3965 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → 𝑝 ⊆ (𝐼‘(𝐺‘𝑆))) |
69 | | simp3r 1201 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆))) |
70 | 68, 69 | pm2.21fal 1564 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑝 ∈ 𝐷 ∧ (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆)))) → ⊥) |
71 | 70 | rexlimdv3a 3217 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (∃𝑝 ∈ 𝐷 (𝑝 ⊆ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ 𝑝 ⊆ (𝐼‘(𝐺‘𝑆))) → ⊥)) |
72 | 28, 71 | syld 47 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → ((𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) → ⊥)) |
73 | 10, 72 | mtoi 198 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → ¬ (𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) |
74 | | dfpss3 4026 |
. . . . . 6
⊢ ((𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆)))) |
75 | 74 | notbii 320 |
. . . . 5
⊢ (¬
(𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ¬ ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆)))) |
76 | | iman 402 |
. . . . 5
⊢ (((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) → ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆))) ↔ ¬ ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ¬ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆)))) |
77 | | anclb 546 |
. . . . 5
⊢ (((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) → ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆))) ↔ ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) → ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆))))) |
78 | 75, 76, 77 | 3bitr2i 299 |
. . . 4
⊢ (¬
(𝐼‘(𝐺‘𝑆)) ⊊ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) → ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆))))) |
79 | 73, 78 | sylib 217 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) → ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆))))) |
80 | 9, 79 | mpd 15 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆)))) |
81 | | eqss 3941 |
. 2
⊢ ((𝐼‘(𝐺‘𝑆)) = ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ∧ ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥) ⊆ (𝐼‘(𝐺‘𝑆)))) |
82 | 80, 81 | sylibr 233 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩
𝑥 ∈ 𝑆 (𝐼‘𝑥)) |