# Metamath Proof Explorer

## Theorem cvrat4

Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in PtakPulmannova p. 68. Also Lemma 9.2(delta) in MaedaMaeda p. 41. ( atcvat4i analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat4.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cvrat4.l
cvrat4.j
cvrat4.z
cvrat4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion cvrat4

### Proof

Step Hyp Ref Expression
1 cvrat4.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cvrat4.l
3 cvrat4.j
4 cvrat4.z
5 cvrat4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
7 6 adantr ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {K}\in \mathrm{AtLat}$
8 simpr1 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {X}\in {B}$
9 1 2 4 5 atlex
10 9 3exp
11 7 8 10 sylc
13 simpll ${⊢}\left(\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\wedge {r}\in {A}\right)\to {K}\in \mathrm{HL}$
14 simplr3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\wedge {r}\in {A}\right)\to {Q}\in {A}$
15 simpr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\wedge {r}\in {A}\right)\to {r}\in {A}$
16 2 3 5 hlatlej1
17 13 14 15 16 syl3anc
18 breq1
19 17 18 syl5ibr
20 19 expd
21 20 impcom
22 21 anim2d
23 22 expcomd
24 23 reximdvai
25 12 24 syld
26 25 ex
27 26 a1i
28 27 com4l
29 28 imp4a
30 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
31 30 adantr ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {K}\in \mathrm{Lat}$
32 simpr3 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {Q}\in {A}$
33 1 5 atbase ${⊢}{Q}\in {A}\to {Q}\in {B}$
34 32 33 syl ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {Q}\in {B}$
35 1 2 3 latleeqj2
36 31 34 8 35 syl3anc
37 36 biimpa
38 37 breq2d
39 38 biimpa
40 39 expl
41 simpl ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {K}\in \mathrm{HL}$
42 simpr2 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {P}\in {A}$
43 2 3 5 hlatlej2
44 41 32 42 43 syl3anc
45 40 44 jctird
46 45 42 jctild
47 46 impl
48 breq1
49 oveq2
50 49 breq2d
51 48 50 anbi12d
52 51 rspcev
53 47 52 syl
55 54 exp31
56 simpr
57 ioran
58 df-ne ${⊢}{P}\ne {Q}↔¬{P}={Q}$
59 58 anbi1i
60 57 59 bitr4i
61 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
62 1 2 3 61 5 cvrat3
63 62 3expd
64 63 imp4c
65 1 5 atbase ${⊢}{P}\in {A}\to {P}\in {B}$
66 42 65 syl ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {P}\in {B}$
67 1 3 latjcl
68 31 66 34 67 syl3anc
69 1 2 61 latmle1
70 31 8 68 69 syl3anc
72 simpll
73 63 imp44
74 simplr2
76 73 74 75 3jca
77 72 76 jca
78 1 2 61 4 5 atnle
79 7 32 8 78 syl3anc
80 1 61 latmcom ${⊢}\left({K}\in \mathrm{Lat}\wedge {Q}\in {B}\wedge {X}\in {B}\right)\to {Q}\mathrm{meet}\left({K}\right){X}={X}\mathrm{meet}\left({K}\right){Q}$
81 31 34 8 80 syl3anc ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {Q}\mathrm{meet}\left({K}\right){X}={X}\mathrm{meet}\left({K}\right){Q}$
82 81 eqeq1d
83 79 82 bitrd
84 1 61 latmcl
85 31 8 68 84 syl3anc
86 85 8 34 3jca
87 31 86 jca
88 1 2 61 latmlem2
89 87 70 88 sylc
90 89 81 breqtrd
91 breq2
92 90 91 syl5ibcom
93 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
94 93 adantr ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\in {B}\wedge {P}\in {A}\wedge {Q}\in {A}\right)\right)\to {K}\in \mathrm{OP}$
95 1 61 latmcl
96 31 34 85 95 syl3anc
97 1 2 4 ople0
98 94 96 97 syl2anc
99 92 98 sylibd
100 83 99 sylbid
101 100 imp
104 1 2 61 latmle2
105 31 8 68 104 syl3anc
106 1 3 latjcom
107 31 66 34 106 syl3anc
108 105 107 breqtrd
111 simpr3
112 simpr1
113 1 5 atbase
114 112 113 syl
115 1 61 latmcom
116 110 111 114 115 syl3anc
117 116 eqeq1d
118 1 2 3 61 4 5 hlexch3
119 118 3expia
120 117 119 sylbid
121 77 103 109 120 syl3c
122 71 121 jca
123 122 ex