Metamath Proof Explorer

Theorem atcvreq0

Description: An element covered by an atom must be zero. ( atcveq0 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses atcvreq0.b 
|- B = ( Base ` K )
atcvreq0.l 
|- .<_ = ( le ` K )
atcvreq0.z 
|- .0. = ( 0. ` K )
atcvreq0.c 
|- C = (
atcvreq0.a 
|- A = ( Atoms ` K )
Assertion atcvreq0 
|- ( ( K e. AtLat /\ X e. B /\ P e. A ) -> ( X C P <-> X = .0. ) )

Proof

Step Hyp Ref Expression
1 atcvreq0.b 
 |-  B = ( Base ` K )
2 atcvreq0.l 
 |-  .<_ = ( le ` K )
3 atcvreq0.z 
 |-  .0. = ( 0. ` K )
4 atcvreq0.c 
 |-  C = (
5 atcvreq0.a 
 |-  A = ( Atoms ` K )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 1 6 3 atl0le 
 |-  ( ( K e. AtLat /\ X e. B ) -> .0. ( le ` K ) X )
8 7 3adant3 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> .0. ( le ` K ) X )
9 8 adantr 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> .0. ( le ` K ) X )
10 1 5 atbase 
 |-  ( P e. A -> P e. B )
11 eqid 
 |-  ( lt ` K ) = ( lt ` K )
12 1 11 4 cvrlt 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. B ) /\ X C P ) -> X ( lt ` K ) P )
13 10 12 syl3anl3 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> X ( lt ` K ) P )
14 atlpos 
 |-  ( K e. AtLat -> K e. Poset )
15 14 3ad2ant1 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> K e. Poset )
16 15 adantr 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> K e. Poset )
17 1 3 atl0cl 
 |-  ( K e. AtLat -> .0. e. B )
18 17 3ad2ant1 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> .0. e. B )
19 18 adantr 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> .0. e. B )
20 10 3ad2ant3 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> P e. B )
21 20 adantr 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> P e. B )
22 simpl2 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> X e. B )
23 3 4 5 atcvr0 
 |-  ( ( K e. AtLat /\ P e. A ) -> .0. C P )
24 23 3adant2 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> .0. C P )
25 24 adantr 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> .0. C P )
26 1 6 11 4 cvrnbtwn3 
 |-  ( ( K e. Poset /\ ( .0. e. B /\ P e. B /\ X e. B ) /\ .0. C P ) -> ( ( .0. ( le ` K ) X /\ X ( lt ` K ) P ) <-> .0. = X ) )
27 16 19 21 22 25 26 syl131anc 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> ( ( .0. ( le ` K ) X /\ X ( lt ` K ) P ) <-> .0. = X ) )
28 9 13 27 mpbi2and 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> .0. = X )
29 28 eqcomd 
 |-  ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ X C P ) -> X = .0. )
30 29 ex 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> ( X C P -> X = .0. ) )
31 breq1 
 |-  ( X = .0. -> ( X C P <-> .0. C P ) )
32 24 31 syl5ibrcom 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> ( X = .0. -> X C P ) )
33 30 32 impbid 
 |-  ( ( K e. AtLat /\ X e. B /\ P e. A ) -> ( X C P <-> X = .0. ) )