Metamath Proof Explorer


Theorem dibintclN

Description: The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibintcl.h 𝐻 = ( LHyp ‘ 𝐾 )
dibintcl.i 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion dibintclN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝑆 ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dibintcl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dibintcl.i 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
3 1 2 dibf11N ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 )
4 3 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 )
5 f1ofn ( 𝐼 : dom 𝐼1-1-onto→ ran 𝐼𝐼 Fn dom 𝐼 )
6 4 5 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝐼 Fn dom 𝐼 )
7 cnvimass ( 𝐼𝑆 ) ⊆ dom 𝐼
8 fnssres ( ( 𝐼 Fn dom 𝐼 ∧ ( 𝐼𝑆 ) ⊆ dom 𝐼 ) → ( 𝐼 ↾ ( 𝐼𝑆 ) ) Fn ( 𝐼𝑆 ) )
9 6 7 8 sylancl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼 ↾ ( 𝐼𝑆 ) ) Fn ( 𝐼𝑆 ) )
10 fniinfv ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) Fn ( 𝐼𝑆 ) → 𝑦 ∈ ( 𝐼𝑆 ) ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) ‘ 𝑦 ) = ran ( 𝐼 ↾ ( 𝐼𝑆 ) ) )
11 9 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝑦 ∈ ( 𝐼𝑆 ) ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) ‘ 𝑦 ) = ran ( 𝐼 ↾ ( 𝐼𝑆 ) ) )
12 df-ima ( 𝐼 “ ( 𝐼𝑆 ) ) = ran ( 𝐼 ↾ ( 𝐼𝑆 ) )
13 f1ofo ( 𝐼 : dom 𝐼1-1-onto→ ran 𝐼𝐼 : dom 𝐼onto→ ran 𝐼 )
14 3 13 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 : dom 𝐼onto→ ran 𝐼 )
15 14 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝐼 : dom 𝐼onto→ ran 𝐼 )
16 simprl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝑆 ⊆ ran 𝐼 )
17 foimacnv ( ( 𝐼 : dom 𝐼onto→ ran 𝐼𝑆 ⊆ ran 𝐼 ) → ( 𝐼 “ ( 𝐼𝑆 ) ) = 𝑆 )
18 15 16 17 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼 “ ( 𝐼𝑆 ) ) = 𝑆 )
19 12 18 eqtr3id ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ran ( 𝐼 ↾ ( 𝐼𝑆 ) ) = 𝑆 )
20 19 inteqd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ran ( 𝐼 ↾ ( 𝐼𝑆 ) ) = 𝑆 )
21 11 20 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝑦 ∈ ( 𝐼𝑆 ) ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) ‘ 𝑦 ) = 𝑆 )
22 simpl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
23 7 a1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼𝑆 ) ⊆ dom 𝐼 )
24 simprr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝑆 ≠ ∅ )
25 n0 ( 𝑆 ≠ ∅ ↔ ∃ 𝑦 𝑦𝑆 )
26 24 25 sylib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ∃ 𝑦 𝑦𝑆 )
27 16 sselda ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → 𝑦 ∈ ran 𝐼 )
28 3 ad2antrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 )
29 28 5 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → 𝐼 Fn dom 𝐼 )
30 fvelrnb ( 𝐼 Fn dom 𝐼 → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ dom 𝐼 ( 𝐼𝑥 ) = 𝑦 ) )
31 29 30 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ dom 𝐼 ( 𝐼𝑥 ) = 𝑦 ) )
32 27 31 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → ∃ 𝑥 ∈ dom 𝐼 ( 𝐼𝑥 ) = 𝑦 )
33 f1ofun ( 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 → Fun 𝐼 )
34 3 33 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → Fun 𝐼 )
35 34 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → Fun 𝐼 )
36 fvimacnv ( ( Fun 𝐼𝑥 ∈ dom 𝐼 ) → ( ( 𝐼𝑥 ) ∈ 𝑆𝑥 ∈ ( 𝐼𝑆 ) ) )
37 35 36 sylan ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ( 𝐼𝑥 ) ∈ 𝑆𝑥 ∈ ( 𝐼𝑆 ) ) )
38 ne0i ( 𝑥 ∈ ( 𝐼𝑆 ) → ( 𝐼𝑆 ) ≠ ∅ )
39 37 38 syl6bi ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ( 𝐼𝑥 ) ∈ 𝑆 → ( 𝐼𝑆 ) ≠ ∅ ) )
40 39 ex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝑥 ∈ dom 𝐼 → ( ( 𝐼𝑥 ) ∈ 𝑆 → ( 𝐼𝑆 ) ≠ ∅ ) ) )
41 eleq1 ( ( 𝐼𝑥 ) = 𝑦 → ( ( 𝐼𝑥 ) ∈ 𝑆𝑦𝑆 ) )
42 41 biimprd ( ( 𝐼𝑥 ) = 𝑦 → ( 𝑦𝑆 → ( 𝐼𝑥 ) ∈ 𝑆 ) )
43 42 imim1d ( ( 𝐼𝑥 ) = 𝑦 → ( ( ( 𝐼𝑥 ) ∈ 𝑆 → ( 𝐼𝑆 ) ≠ ∅ ) → ( 𝑦𝑆 → ( 𝐼𝑆 ) ≠ ∅ ) ) )
44 40 43 syl9 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( ( 𝐼𝑥 ) = 𝑦 → ( 𝑥 ∈ dom 𝐼 → ( 𝑦𝑆 → ( 𝐼𝑆 ) ≠ ∅ ) ) ) )
45 44 com24 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝑦𝑆 → ( 𝑥 ∈ dom 𝐼 → ( ( 𝐼𝑥 ) = 𝑦 → ( 𝐼𝑆 ) ≠ ∅ ) ) ) )
46 45 imp ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → ( 𝑥 ∈ dom 𝐼 → ( ( 𝐼𝑥 ) = 𝑦 → ( 𝐼𝑆 ) ≠ ∅ ) ) )
47 46 rexlimdv ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼𝑥 ) = 𝑦 → ( 𝐼𝑆 ) ≠ ∅ ) )
48 32 47 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦𝑆 ) → ( 𝐼𝑆 ) ≠ ∅ )
49 26 48 exlimddv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼𝑆 ) ≠ ∅ )
50 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
51 50 1 2 dibglbN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐼𝑆 ) ⊆ dom 𝐼 ∧ ( 𝐼𝑆 ) ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ) = 𝑦 ∈ ( 𝐼𝑆 ) ( 𝐼𝑦 ) )
52 22 23 49 51 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ) = 𝑦 ∈ ( 𝐼𝑆 ) ( 𝐼𝑦 ) )
53 fvres ( 𝑦 ∈ ( 𝐼𝑆 ) → ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) ‘ 𝑦 ) = ( 𝐼𝑦 ) )
54 53 iineq2i 𝑦 ∈ ( 𝐼𝑆 ) ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) ‘ 𝑦 ) = 𝑦 ∈ ( 𝐼𝑆 ) ( 𝐼𝑦 )
55 52 54 eqtr4di ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ) = 𝑦 ∈ ( 𝐼𝑆 ) ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) ‘ 𝑦 ) )
56 hlclat ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
57 56 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝐾 ∈ CLat )
58 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
59 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
60 58 59 1 2 dibdmN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → dom 𝐼 = { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } )
61 ssrab2 { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } ⊆ ( Base ‘ 𝐾 )
62 60 61 eqsstrdi ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → dom 𝐼 ⊆ ( Base ‘ 𝐾 ) )
63 62 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → dom 𝐼 ⊆ ( Base ‘ 𝐾 ) )
64 7 63 sstrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼𝑆 ) ⊆ ( Base ‘ 𝐾 ) )
65 58 50 clatglbcl ( ( 𝐾 ∈ CLat ∧ ( 𝐼𝑆 ) ⊆ ( Base ‘ 𝐾 ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
66 57 64 65 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
67 n0 ( ( 𝐼𝑆 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝐼𝑆 ) )
68 49 67 sylib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ∃ 𝑦 𝑦 ∈ ( 𝐼𝑆 ) )
69 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
70 69 ad3antrrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → 𝐾 ∈ Lat )
71 66 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
72 64 sselda ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
73 58 1 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
74 73 ad3antlr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
75 56 ad3antrrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → 𝐾 ∈ CLat )
76 60 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → dom 𝐼 = { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } )
77 7 76 sseqtrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼𝑆 ) ⊆ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } )
78 77 61 sstrdi ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼𝑆 ) ⊆ ( Base ‘ 𝐾 ) )
79 78 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → ( 𝐼𝑆 ) ⊆ ( Base ‘ 𝐾 ) )
80 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → 𝑦 ∈ ( 𝐼𝑆 ) )
81 58 59 50 clatglble ( ( 𝐾 ∈ CLat ∧ ( 𝐼𝑆 ) ⊆ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ( le ‘ 𝐾 ) 𝑦 )
82 75 79 80 81 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ( le ‘ 𝐾 ) 𝑦 )
83 7 sseli ( 𝑦 ∈ ( 𝐼𝑆 ) → 𝑦 ∈ dom 𝐼 )
84 83 adantl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → 𝑦 ∈ dom 𝐼 )
85 58 59 1 2 dibeldmN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑦 ∈ dom 𝐼 ↔ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) )
86 85 ad2antrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → ( 𝑦 ∈ dom 𝐼 ↔ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) )
87 84 86 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) )
88 87 simprd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → 𝑦 ( le ‘ 𝐾 ) 𝑊 )
89 58 59 70 71 72 74 82 88 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ ( 𝐼𝑆 ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ( le ‘ 𝐾 ) 𝑊 )
90 68 89 exlimddv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ( le ‘ 𝐾 ) 𝑊 )
91 58 59 1 2 dibeldmN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ dom 𝐼 ↔ ( ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ( le ‘ 𝐾 ) 𝑊 ) ) )
92 91 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ dom 𝐼 ↔ ( ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ( le ‘ 𝐾 ) 𝑊 ) ) )
93 66 90 92 mpbir2and ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ dom 𝐼 )
94 1 2 dibclN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ) ∈ ran 𝐼 )
95 93 94 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ ( 𝐼𝑆 ) ) ) ∈ ran 𝐼 )
96 55 95 eqeltrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝑦 ∈ ( 𝐼𝑆 ) ( ( 𝐼 ↾ ( 𝐼𝑆 ) ) ‘ 𝑦 ) ∈ ran 𝐼 )
97 21 96 eqeltrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼𝑆 ≠ ∅ ) ) → 𝑆 ∈ ran 𝐼 )