Theorem iscvlat

Description: The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	iscvlat.b	|- B = ( Base ` K )
	iscvlat.l	|- .<_ = ( le ` K )
	iscvlat.j	|- .\/ = ( join ` K )
	iscvlat.a	|- A = ( Atoms ` K )
Assertion	iscvlat	|- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscvlat.b	|- B = ( Base ` K )
2		iscvlat.l	|- .<_ = ( le ` K )
3		iscvlat.j	|- .\/ = ( join ` K )
4		iscvlat.a	|- A = ( Atoms ` K )
5		fveq2	|- ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
6	5 4	eqtr4di	|- ( k = K -> ( Atoms ` k ) = A )
7		fveq2	|- ( k = K -> ( Base ` k ) = ( Base ` K ) )
8	7 1	eqtr4di	|- ( k = K -> ( Base ` k ) = B )
9		fveq2	|- ( k = K -> ( le ` k ) = ( le ` K ) )
10	9 2	eqtr4di	|- ( k = K -> ( le ` k ) = .<_ )
11	10	breqd	|- ( k = K -> ( p ( le ` k ) x <-> p .<_ x ) )
12	11	notbid	|- ( k = K -> ( -. p ( le ` k ) x <-> -. p .<_ x ) )
13		eqidd	|- ( k = K -> p = p )
14		fveq2	|- ( k = K -> ( join ` k ) = ( join ` K ) )
15	14 3	eqtr4di	|- ( k = K -> ( join ` k ) = .\/ )
16	15	oveqd	|- ( k = K -> ( x ( join ` k ) q ) = ( x .\/ q ) )
17	13 10 16	breq123d	|- ( k = K -> ( p ( le ` k ) ( x ( join ` k ) q ) <-> p .<_ ( x .\/ q ) ) )
18	12 17	anbi12d	|- ( k = K -> ( ( -. p ( le ` k ) x /\ p ( le ` k ) ( x ( join ` k ) q ) ) <-> ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) ) )
19		eqidd	|- ( k = K -> q = q )
20	15	oveqd	|- ( k = K -> ( x ( join ` k ) p ) = ( x .\/ p ) )
21	19 10 20	breq123d	|- ( k = K -> ( q ( le ` k ) ( x ( join ` k ) p ) <-> q .<_ ( x .\/ p ) ) )
22	18 21	imbi12d	|- ( k = K -> ( ( ( -. p ( le ` k ) x /\ p ( le ` k ) ( x ( join ` k ) q ) ) -> q ( le ` k ) ( x ( join ` k ) p ) ) <-> ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
23	8 22	raleqbidv	|- ( k = K -> ( A. x e. ( Base ` k ) ( ( -. p ( le ` k ) x /\ p ( le ` k ) ( x ( join ` k ) q ) ) -> q ( le ` k ) ( x ( join ` k ) p ) ) <-> A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
24	6 23	raleqbidv	|- ( k = K -> ( A. q e. ( Atoms ` k ) A. x e. ( Base ` k ) ( ( -. p ( le ` k ) x /\ p ( le ` k ) ( x ( join ` k ) q ) ) -> q ( le ` k ) ( x ( join ` k ) p ) ) <-> A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
25	6 24	raleqbidv	|- ( k = K -> ( A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) A. x e. ( Base ` k ) ( ( -. p ( le ` k ) x /\ p ( le ` k ) ( x ( join ` k ) q ) ) -> q ( le ` k ) ( x ( join ` k ) p ) ) <-> A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
26		df-cvlat	|- CvLat = { k e. AtLat | A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) A. x e. ( Base ` k ) ( ( -. p ( le ` k ) x /\ p ( le ` k ) ( x ( join ` k ) q ) ) -> q ( le ` k ) ( x ( join ` k ) p ) ) }
27	25 26	elrab2	|- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )