Metamath Proof Explorer

Theorem atcvat4i

Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of PtakPulmannova p. 68. (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atcvat3.1 
|- A e. CH
Assertion atcvat4i 
|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) )

Proof

Step Hyp Ref Expression
1 atcvat3.1 
 |-  A e. CH
2 1 hatomici 
 |-  ( A =/= 0H -> E. x e. HAtoms x C_ A )
3 atelch 
 |-  ( C e. HAtoms -> C e. CH )
4 atelch 
 |-  ( x e. HAtoms -> x e. CH )
5 chub1 
 |-  ( ( C e. CH /\ x e. CH ) -> C C_ ( C vH x ) )
6 3 4 5 syl2an 
 |-  ( ( C e. HAtoms /\ x e. HAtoms ) -> C C_ ( C vH x ) )
7 sseq1 
 |-  ( B = C -> ( B C_ ( C vH x ) <-> C C_ ( C vH x ) ) )
8 6 7 imbitrrid 
 |-  ( B = C -> ( ( C e. HAtoms /\ x e. HAtoms ) -> B C_ ( C vH x ) ) )
9 8 expd 
 |-  ( B = C -> ( C e. HAtoms -> ( x e. HAtoms -> B C_ ( C vH x ) ) ) )
10 9 impcom 
 |-  ( ( C e. HAtoms /\ B = C ) -> ( x e. HAtoms -> B C_ ( C vH x ) ) )
11 10 anim2d 
 |-  ( ( C e. HAtoms /\ B = C ) -> ( ( x C_ A /\ x e. HAtoms ) -> ( x C_ A /\ B C_ ( C vH x ) ) ) )
12 11 expcomd 
 |-  ( ( C e. HAtoms /\ B = C ) -> ( x e. HAtoms -> ( x C_ A -> ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
13 12 reximdvai 
 |-  ( ( C e. HAtoms /\ B = C ) -> ( E. x e. HAtoms x C_ A -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) )
14 2 13 syl5 
 |-  ( ( C e. HAtoms /\ B = C ) -> ( A =/= 0H -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) )
15 14 ex 
 |-  ( C e. HAtoms -> ( B = C -> ( A =/= 0H -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
16 15 a1i 
 |-  ( B C_ ( A vH C ) -> ( C e. HAtoms -> ( B = C -> ( A =/= 0H -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) ) )
17 16 com4l 
 |-  ( C e. HAtoms -> ( B = C -> ( A =/= 0H -> ( B C_ ( A vH C ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) ) )
18 17 imp4a 
 |-  ( C e. HAtoms -> ( B = C -> ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
19 18 adantl 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( B = C -> ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
20 atelch 
 |-  ( B e. HAtoms -> B e. CH )
21 chlejb2 
 |-  ( ( C e. CH /\ A e. CH ) -> ( C C_ A <-> ( A vH C ) = A ) )
22 1 21 mpan2 
 |-  ( C e. CH -> ( C C_ A <-> ( A vH C ) = A ) )
23 22 biimpa 
 |-  ( ( C e. CH /\ C C_ A ) -> ( A vH C ) = A )
24 23 sseq2d 
 |-  ( ( C e. CH /\ C C_ A ) -> ( B C_ ( A vH C ) <-> B C_ A ) )
25 24 biimpa 
 |-  ( ( ( C e. CH /\ C C_ A ) /\ B C_ ( A vH C ) ) -> B C_ A )
26 25 expl 
 |-  ( C e. CH -> ( ( C C_ A /\ B C_ ( A vH C ) ) -> B C_ A ) )
27 26 adantl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( ( C C_ A /\ B C_ ( A vH C ) ) -> B C_ A ) )
28 chub2 
 |-  ( ( B e. CH /\ C e. CH ) -> B C_ ( C vH B ) )
29 27 28 jctird 
 |-  ( ( B e. CH /\ C e. CH ) -> ( ( C C_ A /\ B C_ ( A vH C ) ) -> ( B C_ A /\ B C_ ( C vH B ) ) ) )
30 20 3 29 syl2an 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( C C_ A /\ B C_ ( A vH C ) ) -> ( B C_ A /\ B C_ ( C vH B ) ) ) )
31 simpl 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> B e. HAtoms )
32 30 31 jctild 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( C C_ A /\ B C_ ( A vH C ) ) -> ( B e. HAtoms /\ ( B C_ A /\ B C_ ( C vH B ) ) ) ) )
33 32 impl 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ C C_ A ) /\ B C_ ( A vH C ) ) -> ( B e. HAtoms /\ ( B C_ A /\ B C_ ( C vH B ) ) ) )
34 sseq1 
 |-  ( x = B -> ( x C_ A <-> B C_ A ) )
35 oveq2 
 |-  ( x = B -> ( C vH x ) = ( C vH B ) )
36 35 sseq2d 
 |-  ( x = B -> ( B C_ ( C vH x ) <-> B C_ ( C vH B ) ) )
37 34 36 anbi12d 
 |-  ( x = B -> ( ( x C_ A /\ B C_ ( C vH x ) ) <-> ( B C_ A /\ B C_ ( C vH B ) ) ) )
38 37 rspcev 
 |-  ( ( B e. HAtoms /\ ( B C_ A /\ B C_ ( C vH B ) ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) )
39 33 38 syl 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ C C_ A ) /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) )
40 39 adantrl 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ C C_ A ) /\ ( A =/= 0H /\ B C_ ( A vH C ) ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) )
41 40 exp31 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( C C_ A -> ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
42 simpr 
 |-  ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> B C_ ( A vH C ) )
43 ioran 
 |-  ( -. ( B = C \/ C C_ A ) <-> ( -. B = C /\ -. C C_ A ) )
44 1 atcvat3i 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) -> ( A i^i ( B vH C ) ) e. HAtoms ) )
45 3 ad2antlr 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> C e. CH )
46 44 imp 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> ( A i^i ( B vH C ) ) e. HAtoms )
47 simpll 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> B e. HAtoms )
48 45 46 47 3jca 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> ( C e. CH /\ ( A i^i ( B vH C ) ) e. HAtoms /\ B e. HAtoms ) )
49 inss2 
 |-  ( A i^i ( B vH C ) ) C_ ( B vH C )
50 chjcom 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) = ( C vH B ) )
51 20 3 50 syl2an 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( B vH C ) = ( C vH B ) )
52 49 51 sseqtrid 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A i^i ( B vH C ) ) C_ ( C vH B ) )
53 52 adantr 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> ( A i^i ( B vH C ) ) C_ ( C vH B ) )
54 atnssm0 
 |-  ( ( A e. CH /\ C e. HAtoms ) -> ( -. C C_ A <-> ( A i^i C ) = 0H ) )
55 1 54 mpan 
 |-  ( C e. HAtoms -> ( -. C C_ A <-> ( A i^i C ) = 0H ) )
56 55 adantl 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( -. C C_ A <-> ( A i^i C ) = 0H ) )
57 inss1 
 |-  ( A i^i ( B vH C ) ) C_ A
58 sslin 
 |-  ( ( A i^i ( B vH C ) ) C_ A -> ( C i^i ( A i^i ( B vH C ) ) ) C_ ( C i^i A ) )
59 57 58 ax-mp 
 |-  ( C i^i ( A i^i ( B vH C ) ) ) C_ ( C i^i A )
60 incom 
 |-  ( C i^i A ) = ( A i^i C )
61 59 60 sseqtri 
 |-  ( C i^i ( A i^i ( B vH C ) ) ) C_ ( A i^i C )
62 sseq2 
 |-  ( ( A i^i C ) = 0H -> ( ( C i^i ( A i^i ( B vH C ) ) ) C_ ( A i^i C ) <-> ( C i^i ( A i^i ( B vH C ) ) ) C_ 0H ) )
63 61 62 mpbii 
 |-  ( ( A i^i C ) = 0H -> ( C i^i ( A i^i ( B vH C ) ) ) C_ 0H )
64 simpr 
 |-  ( ( B e. CH /\ C e. CH ) -> C e. CH )
65 chjcl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
66 chincl 
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( A i^i ( B vH C ) ) e. CH )
67 1 65 66 sylancr 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A i^i ( B vH C ) ) e. CH )
68 chincl 
 |-  ( ( C e. CH /\ ( A i^i ( B vH C ) ) e. CH ) -> ( C i^i ( A i^i ( B vH C ) ) ) e. CH )
69 64 67 68 syl2anc 
 |-  ( ( B e. CH /\ C e. CH ) -> ( C i^i ( A i^i ( B vH C ) ) ) e. CH )
70 20 3 69 syl2an 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( C i^i ( A i^i ( B vH C ) ) ) e. CH )
71 chle0 
 |-  ( ( C i^i ( A i^i ( B vH C ) ) ) e. CH -> ( ( C i^i ( A i^i ( B vH C ) ) ) C_ 0H <-> ( C i^i ( A i^i ( B vH C ) ) ) = 0H ) )
72 70 71 syl 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( C i^i ( A i^i ( B vH C ) ) ) C_ 0H <-> ( C i^i ( A i^i ( B vH C ) ) ) = 0H ) )
73 63 72 imbitrid 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A i^i C ) = 0H -> ( C i^i ( A i^i ( B vH C ) ) ) = 0H ) )
74 56 73 sylbid 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( -. C C_ A -> ( C i^i ( A i^i ( B vH C ) ) ) = 0H ) )
75 74 imp 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ -. C C_ A ) -> ( C i^i ( A i^i ( B vH C ) ) ) = 0H )
76 75 adantrl 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( -. B = C /\ -. C C_ A ) ) -> ( C i^i ( A i^i ( B vH C ) ) ) = 0H )
77 76 adantrr 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> ( C i^i ( A i^i ( B vH C ) ) ) = 0H )
78 53 77 jca 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> ( ( A i^i ( B vH C ) ) C_ ( C vH B ) /\ ( C i^i ( A i^i ( B vH C ) ) ) = 0H ) )
79 atexch 
 |-  ( ( C e. CH /\ ( A i^i ( B vH C ) ) e. HAtoms /\ B e. HAtoms ) -> ( ( ( A i^i ( B vH C ) ) C_ ( C vH B ) /\ ( C i^i ( A i^i ( B vH C ) ) ) = 0H ) -> B C_ ( C vH ( A i^i ( B vH C ) ) ) ) )
80 48 78 79 sylc 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> B C_ ( C vH ( A i^i ( B vH C ) ) ) )
81 80 57 jctil 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) ) -> ( ( A i^i ( B vH C ) ) C_ A /\ B C_ ( C vH ( A i^i ( B vH C ) ) ) ) )
82 81 ex 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) -> ( ( A i^i ( B vH C ) ) C_ A /\ B C_ ( C vH ( A i^i ( B vH C ) ) ) ) ) )
83 44 82 jcad 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) -> ( ( A i^i ( B vH C ) ) e. HAtoms /\ ( ( A i^i ( B vH C ) ) C_ A /\ B C_ ( C vH ( A i^i ( B vH C ) ) ) ) ) ) )
84 sseq1 
 |-  ( x = ( A i^i ( B vH C ) ) -> ( x C_ A <-> ( A i^i ( B vH C ) ) C_ A ) )
85 oveq2 
 |-  ( x = ( A i^i ( B vH C ) ) -> ( C vH x ) = ( C vH ( A i^i ( B vH C ) ) ) )
86 85 sseq2d 
 |-  ( x = ( A i^i ( B vH C ) ) -> ( B C_ ( C vH x ) <-> B C_ ( C vH ( A i^i ( B vH C ) ) ) ) )
87 84 86 anbi12d 
 |-  ( x = ( A i^i ( B vH C ) ) -> ( ( x C_ A /\ B C_ ( C vH x ) ) <-> ( ( A i^i ( B vH C ) ) C_ A /\ B C_ ( C vH ( A i^i ( B vH C ) ) ) ) ) )
88 87 rspcev 
 |-  ( ( ( A i^i ( B vH C ) ) e. HAtoms /\ ( ( A i^i ( B vH C ) ) C_ A /\ B C_ ( C vH ( A i^i ( B vH C ) ) ) ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) )
89 83 88 syl6 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) )
90 89 expd 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ -. C C_ A ) -> ( B C_ ( A vH C ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
91 43 90 biimtrid 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( -. ( B = C \/ C C_ A ) -> ( B C_ ( A vH C ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
92 42 91 syl7 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( -. ( B = C \/ C C_ A ) -> ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) ) )
93 19 41 92 ecase3d 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) )