Theorem lublecllem

Description: Lemma for lublecl and lubid . (Contributed by NM, 8-Sep-2018)

	Ref	Expression
Hypotheses	lublecl.b	$$⊢B={\mathrm{Base}}_K$$
	lublecl.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lublecl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	lublecl.k	$$⊢\phi \to K\in \mathrm{Poset}$$
	lublecl.x	$$⊢\phi \to X\in B$$
Assertion	lublecllem	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow x=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		lublecl.b	$$⊢B={\mathrm{Base}}_K$$
2		lublecl.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lublecl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lublecl.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		lublecl.x	$$⊢\phi \to X\in B$$
6		breq1	$$⊢y=z\to \left(y\underset{\dot{}}{\le }X\leftrightarrow z\underset{\dot{}}{\le }X\right)$$
7	6	ralrab	$$⊢\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\leftrightarrow \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)$$
8	6	ralrab	$$⊢\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\leftrightarrow \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)$$
9	8	imbi1i	$$⊢\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\leftrightarrow \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)$$
10	9	ralbii	$$⊢\forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\leftrightarrow \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)$$
11	7 10	anbi12i	$$⊢\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\wedge \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\right)$$
12	1 2	posref	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\right)\to X\underset{\dot{}}{\le }X$$
13	4 5 12	syl2anc	$$⊢\phi \to X\underset{\dot{}}{\le }X$$
14		breq1	$$⊢z=X\to \left(z\underset{\dot{}}{\le }X\leftrightarrow X\underset{\dot{}}{\le }X\right)$$
15		breq1	$$⊢z=X\to \left(z\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }x\right)$$
16	14 15	imbi12d	$$⊢z=X\to \left(\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\leftrightarrow \left(X\underset{\dot{}}{\le }X\to X\underset{\dot{}}{\le }x\right)\right)$$
17	16	rspcva	$$⊢\left(X\in B\wedge \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\right)\to \left(X\underset{\dot{}}{\le }X\to X\underset{\dot{}}{\le }x\right)$$
18	13 17	syl5com	$$⊢\phi \to \left(\left(X\in B\wedge \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\right)\to X\underset{\dot{}}{\le }x\right)$$
19	5 18	mpand	$$⊢\phi \to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\to X\underset{\dot{}}{\le }x\right)$$
20	19	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\to X\underset{\dot{}}{\le }x\right)$$
21		idd	$$⊢z\in B\to \left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }X\right)$$
22	21	rgen	$$⊢\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }X\right)$$
23		breq2	$$⊢w=X\to \left(z\underset{\dot{}}{\le }w\leftrightarrow z\underset{\dot{}}{\le }X\right)$$
24	23	imbi2d	$$⊢w=X\to \left(\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\leftrightarrow \left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }X\right)\right)$$
25	24	ralbidv	$$⊢w=X\to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\leftrightarrow \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }X\right)\right)$$
26		breq2	$$⊢w=X\to \left(x\underset{\dot{}}{\le }w\leftrightarrow x\underset{\dot{}}{\le }X\right)$$
27	25 26	imbi12d	$$⊢w=X\to \left(\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\leftrightarrow \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }X\right)\to x\underset{\dot{}}{\le }X\right)\right)$$
28	27	rspcv	$$⊢X\in B\to \left(\forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }X\right)\to x\underset{\dot{}}{\le }X\right)\right)$$
29	5 28	syl	$$⊢\phi \to \left(\forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }X\right)\to x\underset{\dot{}}{\le }X\right)\right)$$
30	22 29	mpii	$$⊢\phi \to \left(\forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }X\right)$$
31	30	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \left(\forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }X\right)$$
32	4	adantr	$$⊢\left(\phi \wedge x\in B\right)\to K\in \mathrm{Poset}$$
33		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
34	5	adantr	$$⊢\left(\phi \wedge x\in B\right)\to X\in B$$
35	1 2	posasymb	$$⊢\left(K\in \mathrm{Poset}\wedge x\in B\wedge X\in B\right)\to \left(\left(x\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\le }x\right)\leftrightarrow x=X\right)$$
36	32 33 34 35	syl3anc	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(x\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\le }x\right)\leftrightarrow x=X\right)$$
37	36	biimpd	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(x\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\le }x\right)\to x=X\right)$$
38	37	ancomsd	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(X\underset{\dot{}}{\le }x\wedge x\underset{\dot{}}{\le }X\right)\to x=X\right)$$
39	20 31 38	syl2and	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\wedge \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\right)\to x=X\right)$$
40		breq2	$$⊢x=X\to \left(z\underset{\dot{}}{\le }x\leftrightarrow z\underset{\dot{}}{\le }X\right)$$
41	40	biimprd	$$⊢x=X\to \left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)$$
42	41	ralrimivw	$$⊢x=X\to \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)$$
43	42	adantl	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge x=X\right)\to \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)$$
44	5	adantr	$$⊢\left(\phi \wedge x=X\right)\to X\in B$$
45		breq1	$$⊢z=X\to \left(z\underset{\dot{}}{\le }w\leftrightarrow X\underset{\dot{}}{\le }w\right)$$
46	14 45	imbi12d	$$⊢z=X\to \left(\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\leftrightarrow \left(X\underset{\dot{}}{\le }X\to X\underset{\dot{}}{\le }w\right)\right)$$
47	46	rspcva	$$⊢\left(X\in B\wedge \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\right)\to \left(X\underset{\dot{}}{\le }X\to X\underset{\dot{}}{\le }w\right)$$
48		pm5.5	$$⊢X\underset{\dot{}}{\le }X\to \left(\left(X\underset{\dot{}}{\le }X\to X\underset{\dot{}}{\le }w\right)\leftrightarrow X\underset{\dot{}}{\le }w\right)$$
49	13 48	syl	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }X\to X\underset{\dot{}}{\le }w\right)\leftrightarrow X\underset{\dot{}}{\le }w\right)$$
50		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }w\leftrightarrow X\underset{\dot{}}{\le }w\right)$$
51	50	bicomd	$$⊢x=X\to \left(X\underset{\dot{}}{\le }w\leftrightarrow x\underset{\dot{}}{\le }w\right)$$
52	49 51	sylan9bb	$$⊢\left(\phi \wedge x=X\right)\to \left(\left(X\underset{\dot{}}{\le }X\to X\underset{\dot{}}{\le }w\right)\leftrightarrow x\underset{\dot{}}{\le }w\right)$$
53	47 52	syl5ib	$$⊢\left(\phi \wedge x=X\right)\to \left(\left(X\in B\wedge \forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\right)\to x\underset{\dot{}}{\le }w\right)$$
54	44 53	mpand	$$⊢\left(\phi \wedge x=X\right)\to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)$$
55	54	ralrimivw	$$⊢\left(\phi \wedge x=X\right)\to \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)$$
56	55	adantlr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge x=X\right)\to \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)$$
57	43 56	jca	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge x=X\right)\to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\wedge \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\right)$$
58	57	ex	$$⊢\left(\phi \wedge x\in B\right)\to \left(x=X\to \left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\wedge \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\right)\right)$$
59	39 58	impbid	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }x\right)\wedge \forall w\in B\left(\forall z\in B\left(z\underset{\dot{}}{\le }X\to z\underset{\dot{}}{\le }w\right)\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow x=X\right)$$
60	11 59	syl5bb	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow x=X\right)$$