Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  atcvr0eq Structured version   Unicode version

Theorem atcvr0eq 30160
 Description: The covers relation is not transitive. (atcv0eq 23874 analog.) (Contributed by NM, 29-Nov-2011.)
Hypotheses
Ref Expression
atcvr0eq.j
atcvr0eq.z
atcvr0eq.c
atcvr0eq.a
Assertion
Ref Expression
atcvr0eq

Proof of Theorem atcvr0eq
StepHypRef Expression
1 atcvr0eq.j . . . . . 6
2 atcvr0eq.c . . . . . 6
3 atcvr0eq.a . . . . . 6
41, 2, 3atcvr1 30151 . . . . 5
5 atcvr0eq.z . . . . . . . 8
65, 2, 3atcvr0 30023 . . . . . . 7
763adant3 977 . . . . . 6
87biantrurd 495 . . . . 5
94, 8bitrd 245 . . . 4
10 simp1 957 . . . . 5
11 hlop 30097 . . . . . . 7
12113ad2ant1 978 . . . . . 6
13 eqid 2435 . . . . . . 7
1413, 5op0cl 29919 . . . . . 6
1512, 14syl 16 . . . . 5
1613, 3atbase 30024 . . . . . 6
17163ad2ant2 979 . . . . 5
1813, 1, 3hlatjcl 30101 . . . . 5
1913, 2cvrntr 30159 . . . . 5
2010, 15, 17, 18, 19syl13anc 1186 . . . 4
219, 20sylbid 207 . . 3