Theorem joinlem

Description: Lemma for join properties. (Contributed by NM, 16-Sep-2011) (Revised by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	joinval2.b	$$⊢B={\mathrm{Base}}_K$$
	joinval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	joinval2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	joinval2.k	$$⊢\phi \to K\in V$$
	joinval2.x	$$⊢\phi \to X\in B$$
	joinval2.y	$$⊢\phi \to Y\in B$$
	joinlem.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
Assertion	joinlem	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		joinval2.b	$$⊢B={\mathrm{Base}}_K$$
2		joinval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		joinval2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		joinval2.k	$$⊢\phi \to K\in V$$
5		joinval2.x	$$⊢\phi \to X\in B$$
6		joinval2.y	$$⊢\phi \to Y\in B$$
7		joinlem.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
8	1 2 3 4 5 6 7	joineu	$$⊢\phi \to \exists !x\in B\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
9		riotasbc	$$⊢\exists !x\in B\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\to \underset{\dot{}}{[}\left(\iota x\in B|\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)/x\underset{\dot{}}{]}\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
10	8 9	syl	$$⊢\phi \to \underset{\dot{}}{[}\left(\iota x\in B|\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)/x\underset{\dot{}}{]}\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
11	1 2 3 4 5 6	joinval2	$$⊢\phi \to X\underset{\dot{}}{\vee }Y=\left(\iota x\in B|\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
12	11	sbceq1d	$$⊢\phi \to \left(\underset{\dot{}}{[}\left(X\underset{\dot{}}{\vee }Y\right)/x\underset{\dot{}}{]}\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \underset{\dot{}}{[}\left(\iota x\in B|\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)/x\underset{\dot{}}{]}\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
13	10 12	mpbird	$$⊢\phi \to \underset{\dot{}}{[}\left(X\underset{\dot{}}{\vee }Y\right)/x\underset{\dot{}}{]}\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
14		ovex	$$⊢X\underset{\dot{}}{\vee }Y\in \mathrm{V}$$
15		breq2	$$⊢x=X\underset{\dot{}}{\vee }Y\to \left(X\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)$$
16		breq2	$$⊢x=X\underset{\dot{}}{\vee }Y\to \left(Y\underset{\dot{}}{\le }x\leftrightarrow Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)$$
17	15 16	anbi12d	$$⊢x=X\underset{\dot{}}{\vee }Y\to \left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\leftrightarrow \left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\right)$$
18		breq1	$$⊢x=X\underset{\dot{}}{\vee }Y\to \left(x\underset{\dot{}}{\le }z\leftrightarrow \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)$$
19	18	imbi2d	$$⊢x=X\underset{\dot{}}{\vee }Y\to \left(\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\right)$$
20	19	ralbidv	$$⊢x=X\underset{\dot{}}{\vee }Y\to \left(\forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\right)$$
21	17 20	anbi12d	$$⊢x=X\underset{\dot{}}{\vee }Y\to \left(\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\right)\right)$$
22	14 21	sbcie	$$⊢\underset{\dot{}}{[}\left(X\underset{\dot{}}{\vee }Y\right)/x\underset{\dot{}}{]}\left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\right)$$
23	13 22	sylib	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\right)$$