Metamath Proof Explorer

Theorem dihglblem6

Description: Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014)

Ref Expression
Hypotheses dihglblem6.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihglblem6.l ⊢ ≤ = ( le ‘ 𝐾 )
dihglblem6.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihglblem6.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihglblem6.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
dihglblem6.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem6.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihglblem6.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihglblem6.s ⊢ 𝑃 = ( LSubSp ‘ 𝑈 )
dihglblem6.d ⊢ 𝐷 = ( LSAtoms ‘ 𝑈 )
Assertion dihglblem6 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 dihglblem6.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihglblem6.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihglblem6.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dihglblem6.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dihglblem6.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
6 dihglblem6.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 dihglblem6.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8 dihglblem6.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 dihglblem6.s ⊢ 𝑃 = ( LSubSp ‘ 𝑈 )
10 dihglblem6.d ⊢ 𝐷 = ( LSAtoms ‘ 𝑈 )
11 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
12 eqid ⊢ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ( meet ‘ 𝐾 ) 𝑊 ) } = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ( meet ‘ 𝐾 ) 𝑊 ) }
13 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
14 1 2 11 5 6 12 13 7 dihglblem4 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
15 fal ⊢ ¬ ⊥
16 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 6 8 16 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → 𝑈 ∈ LMod )
18 simplll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → 𝐾 ∈ HL )
19 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
20 18 19 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → 𝐾 ∈ CLat )
21 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → 𝑆 ⊆ 𝐵 )
22 1 5 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
23 20 21 22 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
24 1 6 7 8 9 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ∈ 𝑃 )
25 16 23 24 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ∈ 𝑃 )
26 1 5 6 8 7 9 dihglblem5 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑃 )
27 26 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑃 )
28 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
29 9 10 17 25 27 28 lpssat ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) → ∃ 𝑝 ∈ 𝐷 ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) )
30 29 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) → ∃ 𝑝 ∈ 𝐷 ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) )
31 simp1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32 6 8 7 10 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ 𝐷 ) → 𝑝 ∈ ran 𝐼 )
33 32 adantlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) → 𝑝 ∈ ran 𝐼 )
34 33 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → 𝑝 ∈ ran 𝐼 )
35 6 7 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) = 𝑝 )
36 31 34 35 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) = 𝑝 )
37 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
38 ssiin ⊢ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 𝑝 ⊆ ( 𝐼 ‘ 𝑥 ) )
39 37 38 sylib ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ∀ 𝑥 ∈ 𝑆 𝑝 ⊆ ( 𝐼 ‘ 𝑥 ) )
40 simplll ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
41 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
42 1 6 7 8 9 dihf11 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 –1-1→ 𝑃 )
43 f1f1orn ⊢ ( 𝐼 : 𝐵 –1-1→ 𝑃 → 𝐼 : 𝐵 –1-1-onto→ ran 𝐼 )
44 41 42 43 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) → 𝐼 : 𝐵 –1-1-onto→ ran 𝐼 )
45 f1ocnvdm ⊢ ( ( 𝐼 : 𝐵 –1-1-onto→ ran 𝐼 ∧ 𝑝 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑝 ) ∈ 𝐵 )
46 44 33 45 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) → ( ◡ 𝐼 ‘ 𝑝 ) ∈ 𝐵 )
47 46 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → ( ◡ 𝐼 ‘ 𝑝 ) ∈ 𝐵 )
48 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) → 𝑆 ⊆ 𝐵 )
49 48 sselda ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
50 1 2 6 7 dihord ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑝 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) ↔ ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 ) )
51 40 47 49 50 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) ↔ ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 ) )
52 41 33 35 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) = 𝑝 )
53 52 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) = 𝑝 )
54 53 sseq1d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) ↔ 𝑝 ⊆ ( 𝐼 ‘ 𝑥 ) ) )
55 51 54 bitr3d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 ↔ 𝑝 ⊆ ( 𝐼 ‘ 𝑥 ) ) )
56 55 ralbidva ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝑆 ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ 𝑆 𝑝 ⊆ ( 𝐼 ‘ 𝑥 ) ) )
57 56 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ 𝑆 𝑝 ⊆ ( 𝐼 ‘ 𝑥 ) ) )
58 39 57 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ∀ 𝑥 ∈ 𝑆 ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 )
59 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → 𝐾 ∈ HL )
60 59 19 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → 𝐾 ∈ CLat )
61 46 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( ◡ 𝐼 ‘ 𝑝 ) ∈ 𝐵 )
62 simp1rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → 𝑆 ⊆ 𝐵 )
63 1 2 5 clatleglb ⊢ ( ( 𝐾 ∈ CLat ∧ ( ◡ 𝐼 ‘ 𝑝 ) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( ( ◡ 𝐼 ‘ 𝑝 ) ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 ) )
64 60 61 62 63 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( ( ◡ 𝐼 ‘ 𝑝 ) ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( ◡ 𝐼 ‘ 𝑝 ) ≤ 𝑥 ) )
65 58 64 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( ◡ 𝐼 ‘ 𝑝 ) ≤ ( 𝐺 ‘ 𝑆 ) )
66 60 62 22 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
67 1 2 6 7 dihord ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑝 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( ◡ 𝐼 ‘ 𝑝 ) ≤ ( 𝐺 ‘ 𝑆 ) ) )
68 31 61 66 67 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( ◡ 𝐼 ‘ 𝑝 ) ≤ ( 𝐺 ‘ 𝑆 ) ) )
69 65 68 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑝 ) ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) )
70 36 69 eqsstrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) )
71 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) )
72 70 71 pm2.21fal ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑝 ∈ 𝐷 ∧ ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) → ⊥ )
73 72 rexlimdv3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( ∃ 𝑝 ∈ 𝐷 ( 𝑝 ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ 𝑝 ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) → ⊥ ) )
74 30 73 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) → ⊥ ) )
75 15 74 mtoi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ¬ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
76 dfpss3 ⊢ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) )
77 76 notbii ⊢ ( ¬ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ¬ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) )
78 iman ⊢ ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) → ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ↔ ¬ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ¬ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) )
79 anclb ⊢ ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) → ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ↔ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) )
80 77 78 79 3bitr2i ⊢ ( ¬ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊊ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) )
81 75 80 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) ) )
82 14 81 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) )
83 eqss ⊢ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∧ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ) )
84 82 83 sylibr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )