lubprlem

Description: Lemma for lubprdm and lubpr . (Contributed by Zhi Wang, 26-Sep-2024)

	Ref	Expression
Hypotheses	lubpr.k	$⊢ φ \to K \in Poset$
	lubpr.b	$⊢ B = {Base}_{K}$
	lubpr.x	$⊢ φ \to X \in B$
	lubpr.y	$⊢ φ \to Y \in B$
	lubpr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lubpr.c	$⊢ φ \to X \underset{˙}{\leq} Y$
	lubpr.s	$⊢ φ \to S = \{X, Y\}$
	lubpr.u	$⊢ U = lub (K)$
Assertion	lubprlem	$⊢ φ \to (S \in dom U \land U (S) = Y)$

Proof

Step	Hyp	Ref	Expression
1		lubpr.k	$⊢ φ \to K \in Poset$
2		lubpr.b	$⊢ B = {Base}_{K}$
3		lubpr.x	$⊢ φ \to X \in B$
4		lubpr.y	$⊢ φ \to Y \in B$
5		lubpr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
6		lubpr.c	$⊢ φ \to X \underset{˙}{\leq} Y$
7		lubpr.s	$⊢ φ \to S = \{X, Y\}$
8		lubpr.u	$⊢ U = lub (K)$
9		breq1	$⊢ z = X \to (z \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\leq} Y)$
10	9 3 6	elrabd	$⊢ φ \to X \in \{z \in B \| z \underset{˙}{\leq} Y\}$
11		breq1	$⊢ z = Y \to (z \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\leq} Y)$
12	2 5	posref	$⊢ (K \in Poset \land Y \in B) \to Y \underset{˙}{\leq} Y$
13	1 4 12	syl2anc	$⊢ φ \to Y \underset{˙}{\leq} Y$
14	11 4 13	elrabd	$⊢ φ \to Y \in \{z \in B \| z \underset{˙}{\leq} Y\}$
15	10 14	prssd	$⊢ φ \to \{X, Y\} \subseteq \{z \in B \| z \underset{˙}{\leq} Y\}$
16	2 5 8 1 4	lublecl	$⊢ φ \to \{z \in B \| z \underset{˙}{\leq} Y\} \in dom U$
17	2 5 8 1 4	lubid	$⊢ φ \to U (\{z \in B \| z \underset{˙}{\leq} Y\}) = Y$
18		prid2g	$⊢ Y \in B \to Y \in \{X, Y\}$
19	4 18	syl	$⊢ φ \to Y \in \{X, Y\}$
20	17 19	eqeltrd	$⊢ φ \to U (\{z \in B \| z \underset{˙}{\leq} Y\}) \in \{X, Y\}$
21	1 15 8 16 20	lubsscl	$⊢ φ \to (\{X, Y\} \in dom U \land U (\{X, Y\}) = U (\{z \in B \| z \underset{˙}{\leq} Y\}))$
22	21	simpld	$⊢ φ \to \{X, Y\} \in dom U$
23	7 22	eqeltrd	$⊢ φ \to S \in dom U$
24	7	fveq2d	$⊢ φ \to U (S) = U (\{X, Y\})$
25	21	simprd	$⊢ φ \to U (\{X, Y\}) = U (\{z \in B \| z \underset{˙}{\leq} Y\})$
26	24 25 17	3eqtrd	$⊢ φ \to U (S) = Y$
27	23 26	jca	$⊢ φ \to (S \in dom U \land U (S) = Y)$

Metamath Proof Explorer

Theorem lubprlem

Proof