dihglblem2aN

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

	Ref	Expression
Hypotheses	dihglblem.b	$⊢ B = {Base}_{K}$
	dihglblem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihglblem.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihglblem.g	$⊢ G = glb (K)$
	dihglblem.h	$⊢ H = LHyp (K)$
	dihglblem.t	$⊢ T = \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
Assertion	dihglblem2aN	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to T \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		dihglblem.b	$⊢ B = {Base}_{K}$
2		dihglblem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihglblem.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dihglblem.g	$⊢ G = glb (K)$
5		dihglblem.h	$⊢ H = LHyp (K)$
6		dihglblem.t	$⊢ T = \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
7	6	a1i	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to T = \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
8		simprr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to S \neq \emptyset$
9		n0	$⊢ S \neq \emptyset \leftrightarrow \exists z z \in S$
10	8 9	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to \exists z z \in S$
11		hllat	$⊢ K \in HL \to K \in Lat$
12	11	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to K \in Lat$
13		simplrl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to S \subseteq B$
14		simpr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to z \in S$
15	13 14	sseldd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to z \in B$
16	1 5	lhpbase	$⊢ W \in H \to W \in B$
17	16	ad3antlr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to W \in B$
18	1 3	latmcl	$⊢ (K \in Lat \land z \in B \land W \in B) \to z \underset{˙}{\land} W \in B$
19	12 15 17 18	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to z \underset{˙}{\land} W \in B$
20		eqidd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to z \underset{˙}{\land} W = z \underset{˙}{\land} W$
21		oveq1	$⊢ v = z \to v \underset{˙}{\land} W = z \underset{˙}{\land} W$
22	21	rspceeqv	$⊢ (z \in S \land z \underset{˙}{\land} W = z \underset{˙}{\land} W) \to \exists v \in S z \underset{˙}{\land} W = v \underset{˙}{\land} W$
23	14 20 22	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to \exists v \in S z \underset{˙}{\land} W = v \underset{˙}{\land} W$
24		ovex	$⊢ z \underset{˙}{\land} W \in V$
25		eleq1	$⊢ w = z \underset{˙}{\land} W \to (w \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \leftrightarrow z \underset{˙}{\land} W \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\})$
26		eqeq1	$⊢ u = z \underset{˙}{\land} W \to (u = v \underset{˙}{\land} W \leftrightarrow z \underset{˙}{\land} W = v \underset{˙}{\land} W)$
27	26	rexbidv	$⊢ u = z \underset{˙}{\land} W \to (\exists v \in S u = v \underset{˙}{\land} W \leftrightarrow \exists v \in S z \underset{˙}{\land} W = v \underset{˙}{\land} W)$
28	27	elrab	$⊢ z \underset{˙}{\land} W \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \leftrightarrow (z \underset{˙}{\land} W \in B \land \exists v \in S z \underset{˙}{\land} W = v \underset{˙}{\land} W)$
29	25 28	bitrdi	$⊢ w = z \underset{˙}{\land} W \to (w \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \leftrightarrow (z \underset{˙}{\land} W \in B \land \exists v \in S z \underset{˙}{\land} W = v \underset{˙}{\land} W))$
30	24 29	spcev	$⊢ (z \underset{˙}{\land} W \in B \land \exists v \in S z \underset{˙}{\land} W = v \underset{˙}{\land} W) \to \exists w w \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
31	19 23 30	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to \exists w w \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
32		n0	$⊢ \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \neq \emptyset \leftrightarrow \exists w w \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
33	31 32	sylibr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land z \in S) \to \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \neq \emptyset$
34	10 33	exlimddv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \neq \emptyset$
35	7 34	eqnetrd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to T \neq \emptyset$

Metamath Proof Explorer

Theorem dihglblem2aN

Proof