Metamath Proof Explorer

Theorem dihglblem4

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

Ref Expression
Hypotheses dihglblem.b ⊢ B = Base K
dihglblem.l ⊢ ≤ ˙ = ≤ K
dihglblem.m ⊢ ∧ ˙ = meet ⁡ K
dihglblem.g ⊢ G = glb ⁡ K
dihglblem.h ⊢ H = LHyp ⁡ K
dihglblem.t ⊢ T = u ∈ B | ∃ v ∈ S u = v ∧ ˙ W
dihglblem.i ⊢ J = DIsoB ⁡ K ⁡ W
dihglblem.ih ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihglblem4 ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ → I ⁡ G ⁡ S ⊆ ⋂ x ∈ S I ⁡ x

Proof

Step Hyp Ref Expression
1 dihglblem.b ⊢ B = Base K
2 dihglblem.l ⊢ ≤ ˙ = ≤ K
3 dihglblem.m ⊢ ∧ ˙ = meet ⁡ K
4 dihglblem.g ⊢ G = glb ⁡ K
5 dihglblem.h ⊢ H = LHyp ⁡ K
6 dihglblem.t ⊢ T = u ∈ B | ∃ v ∈ S u = v ∧ ˙ W
7 dihglblem.i ⊢ J = DIsoB ⁡ K ⁡ W
8 dihglblem.ih ⊢ I = DIsoH ⁡ K ⁡ W
9 hlclat ⊢ K ∈ HL → K ∈ CLat
10 9 ad3antrrr ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → K ∈ CLat
11 simplrl ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → S ⊆ B
12 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → x ∈ S
13 1 2 4 clatglble ⊢ K ∈ CLat ∧ S ⊆ B ∧ x ∈ S → G ⁡ S ≤ ˙ x
14 10 11 12 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → G ⁡ S ≤ ˙ x
15 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → K ∈ HL ∧ W ∈ H
16 1 4 clatglbcl ⊢ K ∈ CLat ∧ S ⊆ B → G ⁡ S ∈ B
17 10 11 16 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → G ⁡ S ∈ B
18 11 12 sseldd ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → x ∈ B
19 1 2 5 8 dihord ⊢ K ∈ HL ∧ W ∈ H ∧ G ⁡ S ∈ B ∧ x ∈ B → I ⁡ G ⁡ S ⊆ I ⁡ x ↔ G ⁡ S ≤ ˙ x
20 15 17 18 19 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → I ⁡ G ⁡ S ⊆ I ⁡ x ↔ G ⁡ S ≤ ˙ x
21 14 20 mpbird ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ x ∈ S → I ⁡ G ⁡ S ⊆ I ⁡ x
22 21 ralrimiva ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ → ∀ x ∈ S I ⁡ G ⁡ S ⊆ I ⁡ x
23 ssiin ⊢ I ⁡ G ⁡ S ⊆ ⋂ x ∈ S I ⁡ x ↔ ∀ x ∈ S I ⁡ G ⁡ S ⊆ I ⁡ x
24 22 23 sylibr ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ → I ⁡ G ⁡ S ⊆ ⋂ x ∈ S I ⁡ x