This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem diaintclN

Description: The intersection of partial isomorphism A closed subspaces is a closed subspace. (Contributed by NM, 3-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diaintcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diaintcl.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diaintclN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∩ 𝑆 ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 diaintcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 diaintcl.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3 1 2 diaf11N ⊢ ( ( 𝐾 ∈ 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 biimtrdi ⊢ ( ( ( ( 𝐾 ∈ 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 diaglbN ⊢ ( ( ( 𝐾 ∈ 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 diadm ⊢ ( ( 𝐾 ∈ 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 diaeldm ⊢ ( ( 𝐾 ∈ 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 diaeldm ⊢ ( ( 𝐾 ∈ 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 diaclN ⊢ ( ( ( 𝐾 ∈ 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 𝐼 )