Theorem joincl

Description: Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		joincl.b	$$⊢B={\mathrm{Base}}_K$$
2		joincl.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		joincl.k	$$⊢\phi \to K\in V$$
4		joincl.x	$$⊢\phi \to X\in B$$
5		joincl.y	$$⊢\phi \to Y\in B$$
6		joincl.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
7		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
8	7 2 3 4 5	joinval	$$⊢\phi \to X\underset{\dot{}}{\vee }Y=\mathrm{lub}\left(K\right)\left(\left\{X,Y\right\}\right)$$
9	7 2 3 4 5	joindef	$$⊢\phi \to \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\leftrightarrow \left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)\right)$$
10	6 9	mpbid	$$⊢\phi \to \left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)$$
11	1 7 3 10	lubcl	$$⊢\phi \to \mathrm{lub}\left(K\right)\left(\left\{X,Y\right\}\right)\in B$$
12	8 11	eqeltrd	$$⊢\phi \to X\underset{\dot{}}{\vee }Y\in B$$