This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chnle

Description: Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sseq2	\|- ( A = if ( A e. CH , A , 0H ) -> ( B C_ A <-> B C_ if ( A e. CH , A , 0H ) ) )
2	1	notbid	\|- ( A = if ( A e. CH , A , 0H ) -> ( -. B C_ A <-> -. B C_ if ( A e. CH , A , 0H ) ) )
3		id	\|- ( A = if ( A e. CH , A , 0H ) -> A = if ( A e. CH , A , 0H ) )
4		oveq1	\|- ( A = if ( A e. CH , A , 0H ) -> ( A vH B ) = ( if ( A e. CH , A , 0H ) vH B ) )
5	3 4	psseq12d	\|- ( A = if ( A e. CH , A , 0H ) -> ( A C. ( A vH B ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) )
6	2 5	bibi12d	\|- ( A = if ( A e. CH , A , 0H ) -> ( ( -. B C_ A <-> A C. ( A vH B ) ) <-> ( -. B C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) ) )
7		sseq1	\|- ( B = if ( B e. CH , B , 0H ) -> ( B C_ if ( A e. CH , A , 0H ) <-> if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) ) )
8	7	notbid	\|- ( B = if ( B e. CH , B , 0H ) -> ( -. B C_ if ( A e. CH , A , 0H ) <-> -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) ) )
9		oveq2	\|- ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) vH B ) = ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) )
10	9	psseq2d	\|- ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) )
11	8 10	bibi12d	\|- ( B = if ( B e. CH , B , 0H ) -> ( ( -. B C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) <-> ( -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) ) )
12		h0elch	\|- 0H e. CH
13	12	elimel	\|- if ( A e. CH , A , 0H ) e. CH
14	12	elimel	\|- if ( B e. CH , B , 0H ) e. CH
15	13 14	chnlei	\|- ( -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) )
16	6 11 15	dedth2h	\|- ( ( A e. CH /\ B e. CH ) -> ( -. B C_ A <-> A C. ( A vH B ) ) )