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 ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
diaintcl.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
Assertion diaintclN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap {S}\in \mathrm{ran}{I}$

Proof

Step Hyp Ref Expression
1 diaintcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 diaintcl.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
3 1 2 diaf11N ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$
4 3 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$
5 f1ofn ${⊢}{I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}\to {I}Fn\mathrm{dom}{I}$
6 4 5 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}Fn\mathrm{dom}{I}$
7 cnvimass ${⊢}{{I}}^{-1}\left[{S}\right]\subseteq \mathrm{dom}{I}$
8 fnssres ${⊢}\left({I}Fn\mathrm{dom}{I}\wedge {{I}}^{-1}\left[{S}\right]\subseteq \mathrm{dom}{I}\right)\to \left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)Fn{{I}}^{-1}\left[{S}\right]$
9 6 7 8 sylancl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)Fn{{I}}^{-1}\left[{S}\right]$
10 fniinfv ${⊢}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)Fn{{I}}^{-1}\left[{S}\right]\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)$
11 9 10 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)$
12 df-ima ${⊢}{I}\left[{{I}}^{-1}\left[{S}\right]\right]=\mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)$
13 f1ofo ${⊢}{I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}\to {I}:\mathrm{dom}{I}\underset{onto}{⟶}\mathrm{ran}{I}$
14 3 13 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{onto}{⟶}\mathrm{ran}{I}$
15 14 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}:\mathrm{dom}{I}\underset{onto}{⟶}\mathrm{ran}{I}$
16 simprl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq \mathrm{ran}{I}$
17 foimacnv ${⊢}\left({I}:\mathrm{dom}{I}\underset{onto}{⟶}\mathrm{ran}{I}\wedge {S}\subseteq \mathrm{ran}{I}\right)\to {I}\left[{{I}}^{-1}\left[{S}\right]\right]={S}$
18 15 16 17 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left[{{I}}^{-1}\left[{S}\right]\right]={S}$
19 12 18 syl5eqr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)={S}$
20 19 inteqd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap \mathrm{ran}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)=\bigcap {S}$
21 11 20 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap {S}$
22 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
23 7 a1i ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {{I}}^{-1}\left[{S}\right]\subseteq \mathrm{dom}{I}$
24 simprr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {S}\ne \varnothing$
25 n0 ${⊢}{S}\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {S}$
26 24 25 sylib ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {S}$
27 16 sselda ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {y}\in \mathrm{ran}{I}$
28 3 ad2antrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$
29 28 5 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {I}Fn\mathrm{dom}{I}$
30 fvelrnb ${⊢}{I}Fn\mathrm{dom}{I}\to \left({y}\in \mathrm{ran}{I}↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}\right)$
31 29 30 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \left({y}\in \mathrm{ran}{I}↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}\right)$
32 27 31 mpbid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}$
33 f1ofun ${⊢}{I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}\to \mathrm{Fun}{I}$
34 3 33 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{Fun}{I}$
35 34 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{Fun}{I}$
36 fvimacnv ${⊢}\left(\mathrm{Fun}{I}\wedge {x}\in \mathrm{dom}{I}\right)\to \left({I}\left({x}\right)\in {S}↔{x}\in {{I}}^{-1}\left[{S}\right]\right)$
37 35 36 sylan ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in \mathrm{dom}{I}\right)\to \left({I}\left({x}\right)\in {S}↔{x}\in {{I}}^{-1}\left[{S}\right]\right)$
38 ne0i ${⊢}{x}\in {{I}}^{-1}\left[{S}\right]\to {{I}}^{-1}\left[{S}\right]\ne \varnothing$
39 37 38 syl6bi ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in \mathrm{dom}{I}\right)\to \left({I}\left({x}\right)\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)$
40 39 ex ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({x}\in \mathrm{dom}{I}\to \left({I}\left({x}\right)\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)$
41 eleq1 ${⊢}{I}\left({x}\right)={y}\to \left({I}\left({x}\right)\in {S}↔{y}\in {S}\right)$
42 41 biimprd ${⊢}{I}\left({x}\right)={y}\to \left({y}\in {S}\to {I}\left({x}\right)\in {S}\right)$
43 42 imim1d ${⊢}{I}\left({x}\right)={y}\to \left(\left({I}\left({x}\right)\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\to \left({y}\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)$
44 40 43 syl9 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({I}\left({x}\right)={y}\to \left({x}\in \mathrm{dom}{I}\to \left({y}\in {S}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)\right)$
45 44 com24 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({y}\in {S}\to \left({x}\in \mathrm{dom}{I}\to \left({I}\left({x}\right)={y}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)\right)$
46 45 imp ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \left({x}\in \mathrm{dom}{I}\to \left({I}\left({x}\right)={y}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)$
47 46 rexlimdv ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to \left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)={y}\to {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)$
48 32 47 mpd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {{I}}^{-1}\left[{S}\right]\ne \varnothing$
49 26 48 exlimddv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {{I}}^{-1}\left[{S}\right]\ne \varnothing$
50 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
51 50 1 2 diaglbN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({{I}}^{-1}\left[{S}\right]\subseteq \mathrm{dom}{I}\wedge {{I}}^{-1}\left[{S}\right]\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}{I}\left({y}\right)$
52 22 23 49 51 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}{I}\left({y}\right)$
53 fvres ${⊢}{y}\in {{I}}^{-1}\left[{S}\right]\to \left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)={I}\left({y}\right)$
54 53 iineq2i ${⊢}\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}{I}\left({y}\right)$
55 52 54 syl6eqr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)=\bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)$
56 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
57 56 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {K}\in \mathrm{CLat}$
58 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
59 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
60 58 59 1 2 diadm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{dom}{I}=\left\{{x}\in {\mathrm{Base}}_{{K}}|{x}{\le }_{{K}}{W}\right\}$
61 ssrab2 ${⊢}\left\{{x}\in {\mathrm{Base}}_{{K}}|{x}{\le }_{{K}}{W}\right\}\subseteq {\mathrm{Base}}_{{K}}$
62 60 61 eqsstrdi ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{dom}{I}\subseteq {\mathrm{Base}}_{{K}}$
63 62 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{dom}{I}\subseteq {\mathrm{Base}}_{{K}}$
64 7 63 sstrid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}$
65 58 50 clatglbcl ${⊢}\left({K}\in \mathrm{CLat}\wedge {{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}$
66 57 64 65 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}$
67 n0 ${⊢}{{I}}^{-1}\left[{S}\right]\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {{I}}^{-1}\left[{S}\right]$
68 49 67 sylib ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {{I}}^{-1}\left[{S}\right]$
69 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
70 69 ad3antrrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {K}\in \mathrm{Lat}$
71 66 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}$
72 64 sselda ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {y}\in {\mathrm{Base}}_{{K}}$
73 58 1 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
74 73 ad3antlr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {W}\in {\mathrm{Base}}_{{K}}$
75 56 ad3antrrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {K}\in \mathrm{CLat}$
76 60 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{dom}{I}=\left\{{x}\in {\mathrm{Base}}_{{K}}|{x}{\le }_{{K}}{W}\right\}$
77 7 76 sseqtrid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {{I}}^{-1}\left[{S}\right]\subseteq \left\{{x}\in {\mathrm{Base}}_{{K}}|{x}{\le }_{{K}}{W}\right\}$
78 77 61 sstrdi ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}$
79 78 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}$
80 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {y}\in {{I}}^{-1}\left[{S}\right]$
81 58 59 50 clatglble ${⊢}\left({K}\in \mathrm{CLat}\wedge {{I}}^{-1}\left[{S}\right]\subseteq {\mathrm{Base}}_{{K}}\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right){\le }_{{K}}{y}$
82 75 79 80 81 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right){\le }_{{K}}{y}$
83 7 sseli ${⊢}{y}\in {{I}}^{-1}\left[{S}\right]\to {y}\in \mathrm{dom}{I}$
84 83 adantl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {y}\in \mathrm{dom}{I}$
85 58 59 1 2 diaeldm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({y}\in \mathrm{dom}{I}↔\left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)\right)$
86 85 ad2antrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to \left({y}\in \mathrm{dom}{I}↔\left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)\right)$
87 84 86 mpbid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to \left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)$
88 87 simprd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to {y}{\le }_{{K}}{W}$
89 58 59 70 71 72 74 82 88 lattrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {{I}}^{-1}\left[{S}\right]\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right){\le }_{{K}}{W}$
90 68 89 exlimddv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right){\le }_{{K}}{W}$
91 58 59 1 2 diaeldm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in \mathrm{dom}{I}↔\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right){\le }_{{K}}{W}\right)\right)$
92 91 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in \mathrm{dom}{I}↔\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right){\le }_{{K}}{W}\right)\right)$
93 66 90 92 mpbir2and ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in \mathrm{dom}{I}$
94 1 2 diaclN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\in \mathrm{dom}{I}\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)\in \mathrm{ran}{I}$
95 93 94 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left({{I}}^{-1}\left[{S}\right]\right)\right)\in \mathrm{ran}{I}$
96 55 95 eqeltrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap _{{y}\in {{I}}^{-1}\left[{S}\right]}\left({{I}↾}_{{{I}}^{-1}\left[{S}\right]}\right)\left({y}\right)\in \mathrm{ran}{I}$
97 21 96 eqeltrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{ran}{I}\wedge {S}\ne \varnothing \right)\right)\to \bigcap {S}\in \mathrm{ran}{I}$