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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑇 ≠ ∅ )