Theorem chlub

Description: Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chlub	|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) )

Proof

Step	Hyp	Ref	Expression
1		chsh	|- ( A e. CH -> A e. SH )
2		chsh	|- ( B e. CH -> B e. SH )
3		shlub	|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) )
4	2 3	syl3an2	|- ( ( A e. SH /\ B e. CH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) )
5	1 4	syl3an1	|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) )