Metamath Proof Explorer


Theorem eliccelico

Description: Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017)

Ref Expression
Assertion eliccelico A*B*ABCABCABC=B

Proof

Step Hyp Ref Expression
1 simpl1 A*B*ABCAB¬CABA*
2 simpl2 A*B*ABCAB¬CABB*
3 simprl A*B*ABCAB¬CABCAB
4 elicc1 A*B*CABC*ACCB
5 4 biimpa A*B*CABC*ACCB
6 5 simp1d A*B*CABC*
7 1 2 3 6 syl21anc A*B*ABCAB¬CABC*
8 5 simp3d A*B*CABCB
9 1 2 3 8 syl21anc A*B*ABCAB¬CABCB
10 1 2 jca A*B*ABCAB¬CABA*B*
11 simprr A*B*ABCAB¬CAB¬CAB
12 5 simp2d A*B*CABAC
13 10 3 12 syl2anc A*B*ABCAB¬CABAC
14 elico1 A*B*CABC*ACC<B
15 14 notbid A*B*¬CAB¬C*ACC<B
16 15 biimpa A*B*¬CAB¬C*ACC<B
17 df-3an C*ACC<BC*ACC<B
18 17 notbii ¬C*ACC<B¬C*ACC<B
19 imnan C*AC¬C<B¬C*ACC<B
20 18 19 bitr4i ¬C*ACC<BC*AC¬C<B
21 16 20 sylib A*B*¬CABC*AC¬C<B
22 21 imp A*B*¬CABC*AC¬C<B
23 10 11 7 13 22 syl22anc A*B*ABCAB¬CAB¬C<B
24 xeqlelt C*B*C=BCB¬C<B
25 24 biimpar C*B*CB¬C<BC=B
26 7 2 9 23 25 syl22anc A*B*ABCAB¬CABC=B
27 26 ex A*B*ABCAB¬CABC=B
28 pm5.6 CAB¬CABC=BCABCABC=B
29 27 28 sylib A*B*ABCABCABC=B
30 icossicc ABAB
31 simpr A*B*ABCABCAB
32 30 31 sselid A*B*ABCABCAB
33 simpr A*B*ABC=BC=B
34 simpl2 A*B*ABC=BB*
35 33 34 eqeltrd A*B*ABC=BC*
36 simpl3 A*B*ABC=BAB
37 36 33 breqtrrd A*B*ABC=BAC
38 34 xrleidd A*B*ABC=BBB
39 33 38 eqbrtrd A*B*ABC=BCB
40 simpl1 A*B*ABC=BA*
41 40 34 4 syl2anc A*B*ABC=BCABC*ACCB
42 35 37 39 41 mpbir3and A*B*ABC=BCAB
43 32 42 jaodan A*B*ABCABC=BCAB
44 43 ex A*B*ABCABC=BCAB
45 29 44 impbid A*B*ABCABCABC=B