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

Metamath Proof Explorer

Theorem dihglblem2aN

Description: Lemma for isomorphism H of a GLB. (Contributed by NM, 19-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihglblem.l ⊢ ≤ = ( le ‘ 𝐾 )
dihglblem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihglblem.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
dihglblem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem.t ⊢ 𝑇 = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) }
Assertion dihglblem2aN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑇 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 dihglblem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihglblem.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihglblem.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dihglblem.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
5 dihglblem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dihglblem.t ⊢ 𝑇 = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) }
7 6 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑇 = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } )
8 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ≠ ∅ )
9 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝑆 )
10 8 9 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ∃ 𝑧 𝑧 ∈ 𝑆 )
11 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
12 11 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝐾 ∈ Lat )
13 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
14 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
15 13 14 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝐵 )
16 1 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
17 16 ad3antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑊 ∈ 𝐵 )
18 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑧 ∧ 𝑊 ) ∈ 𝐵 )
19 12 15 17 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 ∧ 𝑊 ) ∈ 𝐵 )
20 eqidd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 ∧ 𝑊 ) = ( 𝑧 ∧ 𝑊 ) )
21 oveq1 ⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∧ 𝑊 ) = ( 𝑧 ∧ 𝑊 ) )
22 21 rspceeqv ⊢ ( ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ∧ 𝑊 ) = ( 𝑧 ∧ 𝑊 ) ) → ∃ 𝑣 ∈ 𝑆 ( 𝑧 ∧ 𝑊 ) = ( 𝑣 ∧ 𝑊 ) )
23 14 20 22 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → ∃ 𝑣 ∈ 𝑆 ( 𝑧 ∧ 𝑊 ) = ( 𝑣 ∧ 𝑊 ) )
24 ovex ⊢ ( 𝑧 ∧ 𝑊 ) ∈ V
25 eleq1 ⊢ ( 𝑤 = ( 𝑧 ∧ 𝑊 ) → ( 𝑤 ∈ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ↔ ( 𝑧 ∧ 𝑊 ) ∈ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ) )
26 eqeq1 ⊢ ( 𝑢 = ( 𝑧 ∧ 𝑊 ) → ( 𝑢 = ( 𝑣 ∧ 𝑊 ) ↔ ( 𝑧 ∧ 𝑊 ) = ( 𝑣 ∧ 𝑊 ) ) )
27 26 rexbidv ⊢ ( 𝑢 = ( 𝑧 ∧ 𝑊 ) → ( ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) ↔ ∃ 𝑣 ∈ 𝑆 ( 𝑧 ∧ 𝑊 ) = ( 𝑣 ∧ 𝑊 ) ) )
28 27 elrab ⊢ ( ( 𝑧 ∧ 𝑊 ) ∈ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ↔ ( ( 𝑧 ∧ 𝑊 ) ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝑧 ∧ 𝑊 ) = ( 𝑣 ∧ 𝑊 ) ) )
29 25 28 bitrdi ⊢ ( 𝑤 = ( 𝑧 ∧ 𝑊 ) → ( 𝑤 ∈ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ↔ ( ( 𝑧 ∧ 𝑊 ) ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝑧 ∧ 𝑊 ) = ( 𝑣 ∧ 𝑊 ) ) ) )
30 24 29 spcev ⊢ ( ( ( 𝑧 ∧ 𝑊 ) ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝑧 ∧ 𝑊 ) = ( 𝑣 ∧ 𝑊 ) ) → ∃ 𝑤 𝑤 ∈ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } )
31 19 23 30 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → ∃ 𝑤 𝑤 ∈ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } )
32 n0 ⊢ ( { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } )
33 31 32 sylibr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑧 ∈ 𝑆 ) → { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ≠ ∅ )
34 10 33 exlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ≠ ∅ )
35 7 34 eqnetrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑇 ≠ ∅ )