# Metamath Proof Explorer

## Theorem dibglbN

Description: Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibglb.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
dibglb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dibglb.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
Assertion dibglbN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}{I}\left({x}\right)$

### Proof

Step Hyp Ref Expression
1 dibglb.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
2 dibglb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dibglb.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
4 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
5 simprl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}{I}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq \mathrm{dom}{I}$
6 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
7 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
8 6 7 2 3 dibdmN ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{dom}{I}=\left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}$
9 8 sseq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({S}\subseteq \mathrm{dom}{I}↔{S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\right)$
10 9 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}{I}\wedge {S}\ne \varnothing \right)\right)\to \left({S}\subseteq \mathrm{dom}{I}↔{S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\right)$
11 5 10 mpbid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}{I}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}$
12 simprr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}{I}\wedge {S}\ne \varnothing \right)\right)\to {S}\ne \varnothing$
13 2 3 dibvalrel ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{Rel}{I}\left({G}\left({S}\right)\right)$
14 13 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{Rel}{I}\left({G}\left({S}\right)\right)$
15 n0 ${⊢}{S}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {S}$
16 15 biimpi ${⊢}{S}\ne \varnothing \to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {S}$
17 16 ad2antll ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {S}$
18 2 3 dibvalrel ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{Rel}{I}\left({x}\right)$
19 18 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{Rel}{I}\left({x}\right)$
20 19 a1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left({x}\in {S}\to \mathrm{Rel}{I}\left({x}\right)\right)$
21 20 ancld ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left({x}\in {S}\to \left({x}\in {S}\wedge \mathrm{Rel}{I}\left({x}\right)\right)\right)$
22 21 eximdv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {S}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}\wedge \mathrm{Rel}{I}\left({x}\right)\right)\right)$
23 17 22 mpd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}\wedge \mathrm{Rel}{I}\left({x}\right)\right)$
24 df-rex ${⊢}\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}{I}\left({x}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}\wedge \mathrm{Rel}{I}\left({x}\right)\right)$
25 23 24 sylibr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}{I}\left({x}\right)$
26 reliin ${⊢}\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}{I}\left({x}\right)\to \mathrm{Rel}\bigcap _{{x}\in {S}}{I}\left({x}\right)$
27 25 26 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{Rel}\bigcap _{{x}\in {S}}{I}\left({x}\right)$
28 id ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)$
29 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
30 simprl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}$
31 eqid ${⊢}\mathrm{DIsoA}\left({K}\right)\left({W}\right)=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
32 6 7 2 31 diadm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{dom}\mathrm{DIsoA}\left({K}\right)\left({W}\right)=\left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}$
33 32 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{dom}\mathrm{DIsoA}\left({K}\right)\left({W}\right)=\left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}$
34 30 33 sseqtrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq \mathrm{dom}\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
35 simprr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {S}\ne \varnothing$
36 1 2 31 diaglbN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}\mathrm{DIsoA}\left({K}\right)\left({W}\right)\wedge {S}\ne \varnothing \right)\right)\to \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)$
37 29 34 35 36 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)$
38 37 eleq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)↔{f}\in \bigcap _{{x}\in {S}}\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\right)$
39 vex ${⊢}{f}\in \mathrm{V}$
40 eliin ${⊢}{f}\in \mathrm{V}\to \left({f}\in \bigcap _{{x}\in {S}}\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\right)$
41 39 40 ax-mp ${⊢}{f}\in \bigcap _{{x}\in {S}}\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)$
42 38 41 syl6bb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\right)$
43 42 anbi1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)↔\left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
44 r19.27zv ${⊢}{S}\ne \varnothing \to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)↔\left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
45 44 ad2antll ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)↔\left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
46 43 45 bitr4d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
47 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
48 47 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {K}\in \mathrm{CLat}$
49 ssrab2 ${⊢}\left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\subseteq {\mathrm{Base}}_{{K}}$
50 30 49 sstrdi ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq {\mathrm{Base}}_{{K}}$
51 6 1 clatglbcl ${⊢}\left({K}\in \mathrm{CLat}\wedge {S}\subseteq {\mathrm{Base}}_{{K}}\right)\to {G}\left({S}\right)\in {\mathrm{Base}}_{{K}}$
52 48 50 51 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {G}\left({S}\right)\in {\mathrm{Base}}_{{K}}$
53 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
54 53 ad3antrrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {K}\in \mathrm{Lat}$
55 47 ad3antrrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {K}\in \mathrm{CLat}$
56 simplrl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}$
57 56 49 sstrdi ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {S}\subseteq {\mathrm{Base}}_{{K}}$
58 55 57 51 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {G}\left({S}\right)\in {\mathrm{Base}}_{{K}}$
59 50 sselda ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {x}\in {\mathrm{Base}}_{{K}}$
60 6 2 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
61 60 ad3antlr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {W}\in {\mathrm{Base}}_{{K}}$
62 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {x}\in {S}$
63 6 7 1 clatglble ${⊢}\left({K}\in \mathrm{CLat}\wedge {S}\subseteq {\mathrm{Base}}_{{K}}\wedge {x}\in {S}\right)\to {G}\left({S}\right){\le }_{{K}}{x}$
64 55 57 62 63 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {G}\left({S}\right){\le }_{{K}}{x}$
65 30 sselda ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {x}\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}$
66 breq1 ${⊢}{y}={x}\to \left({y}{\le }_{{K}}{W}↔{x}{\le }_{{K}}{W}\right)$
67 66 elrab ${⊢}{x}\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}↔\left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)$
68 65 67 sylib ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to \left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)$
69 68 simprd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {x}{\le }_{{K}}{W}$
70 6 7 54 58 59 61 64 69 lattrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {G}\left({S}\right){\le }_{{K}}{W}$
71 17 70 exlimddv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {G}\left({S}\right){\le }_{{K}}{W}$
72 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
73 eqid ${⊢}\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)$
74 6 7 2 72 73 31 3 dibopelval2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({G}\left({S}\right)\in {\mathrm{Base}}_{{K}}\wedge {G}\left({S}\right){\le }_{{K}}{W}\right)\right)\to \left(⟨{f},{s}⟩\in {I}\left({G}\left({S}\right)\right)↔\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
75 29 52 71 74 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(⟨{f},{s}⟩\in {I}\left({G}\left({S}\right)\right)↔\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({G}\left({S}\right)\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
76 opex ${⊢}⟨{f},{s}⟩\in \mathrm{V}$
77 eliin ${⊢}⟨{f},{s}⟩\in \mathrm{V}\to \left(⟨{f},{s}⟩\in \bigcap _{{x}\in {S}}{I}\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}⟨{f},{s}⟩\in {I}\left({x}\right)\right)$
78 76 77 ax-mp ${⊢}⟨{f},{s}⟩\in \bigcap _{{x}\in {S}}{I}\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}⟨{f},{s}⟩\in {I}\left({x}\right)$
79 simpll ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
80 6 7 2 72 73 31 3 dibopelval2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)\right)\to \left(⟨{f},{s}⟩\in {I}\left({x}\right)↔\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
81 79 68 80 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to \left(⟨{f},{s}⟩\in {I}\left({x}\right)↔\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
82 81 ralbidva ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}⟨{f},{s}⟩\in {I}\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
83 78 82 syl5bb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(⟨{f},{s}⟩\in \bigcap _{{x}\in {S}}{I}\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({x}\right)\wedge {s}=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)\right)\right)$
84 46 75 83 3bitr4d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to \left(⟨{f},{s}⟩\in {I}\left({G}\left({S}\right)\right)↔⟨{f},{s}⟩\in \bigcap _{{x}\in {S}}{I}\left({x}\right)\right)$
85 84 eqrelrdv2 ${⊢}\left(\left(\mathrm{Rel}{I}\left({G}\left({S}\right)\right)\wedge \mathrm{Rel}\bigcap _{{x}\in {S}}{I}\left({x}\right)\right)\wedge \left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\right)\to {I}\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}{I}\left({x}\right)$
86 14 27 28 85 syl21anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \left\{{y}\in {\mathrm{Base}}_{{K}}|{y}{\le }_{{K}}{W}\right\}\wedge {S}\ne \varnothing \right)\right)\to {I}\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}{I}\left({x}\right)$
87 4 11 12 86 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq \mathrm{dom}{I}\wedge {S}\ne \varnothing \right)\right)\to {I}\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}{I}\left({x}\right)$