Metamath Proof Explorer

Theorem toslublem

Description: Lemma for toslub and xrsclat . (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by NM, 15-Sep-2018)

Ref Expression
Hypotheses toslub.b 
|- B = ( Base ` K )
toslub.l 
|- .< = ( lt ` K )
toslub.1 
|- ( ph -> K e. Toset )
toslub.2 
|- ( ph -> A C_ B )
toslub.e 
|- .<_ = ( le ` K )
Assertion toslublem 
|- ( ( ph /\ a e. B ) -> ( ( A. b e. A b .<_ a /\ A. c e. B ( A. b e. A b .<_ c -> a .<_ c ) ) <-> ( A. b e. A -. a .< b /\ A. b e. B ( b .< a -> E. d e. A b .< d ) ) ) )

Proof

Step Hyp Ref Expression
1 toslub.b 
 |-  B = ( Base ` K )
2 toslub.l 
 |-  .< = ( lt ` K )
3 toslub.1 
 |-  ( ph -> K e. Toset )
4 toslub.2 
 |-  ( ph -> A C_ B )
5 toslub.e 
 |-  .<_ = ( le ` K )
6 3 ad2antrr 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> K e. Toset )
7 simplr 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> a e. B )
8 4 adantr 
 |-  ( ( ph /\ a e. B ) -> A C_ B )
9 8 sselda 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> b e. B )
10 1 5 2 tltnle 
 |-  ( ( K e. Toset /\ a e. B /\ b e. B ) -> ( a .< b <-> -. b .<_ a ) )
11 6 7 9 10 syl3anc 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> ( a .< b <-> -. b .<_ a ) )
12 11 con2bid 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> ( b .<_ a <-> -. a .< b ) )
13 12 ralbidva 
 |-  ( ( ph /\ a e. B ) -> ( A. b e. A b .<_ a <-> A. b e. A -. a .< b ) )
14 4 ad2antrr 
 |-  ( ( ( ph /\ c e. B ) /\ b e. A ) -> A C_ B )
15 simpr 
 |-  ( ( ( ph /\ c e. B ) /\ b e. A ) -> b e. A )
16 14 15 sseldd 
 |-  ( ( ( ph /\ c e. B ) /\ b e. A ) -> b e. B )
17 1 5 2 tltnle 
 |-  ( ( K e. Toset /\ c e. B /\ b e. B ) -> ( c .< b <-> -. b .<_ c ) )
18 3 17 syl3an1 
 |-  ( ( ph /\ c e. B /\ b e. B ) -> ( c .< b <-> -. b .<_ c ) )
19 18 3expa 
 |-  ( ( ( ph /\ c e. B ) /\ b e. B ) -> ( c .< b <-> -. b .<_ c ) )
20 19 con2bid 
 |-  ( ( ( ph /\ c e. B ) /\ b e. B ) -> ( b .<_ c <-> -. c .< b ) )
21 16 20 syldan 
 |-  ( ( ( ph /\ c e. B ) /\ b e. A ) -> ( b .<_ c <-> -. c .< b ) )
22 21 ralbidva 
 |-  ( ( ph /\ c e. B ) -> ( A. b e. A b .<_ c <-> A. b e. A -. c .< b ) )
23 breq2 
 |-  ( b = d -> ( c .< b <-> c .< d ) )
24 23 notbid 
 |-  ( b = d -> ( -. c .< b <-> -. c .< d ) )
25 24 cbvralvw 
 |-  ( A. b e. A -. c .< b <-> A. d e. A -. c .< d )
26 ralnex 
 |-  ( A. d e. A -. c .< d <-> -. E. d e. A c .< d )
27 25 26 bitri 
 |-  ( A. b e. A -. c .< b <-> -. E. d e. A c .< d )
28 22 27 bitrdi 
 |-  ( ( ph /\ c e. B ) -> ( A. b e. A b .<_ c <-> -. E. d e. A c .< d ) )
29 28 adantlr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( A. b e. A b .<_ c <-> -. E. d e. A c .< d ) )
30 3 ad2antrr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> K e. Toset )
31 simpr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> c e. B )
32 simplr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> a e. B )
33 1 5 2 tltnle 
 |-  ( ( K e. Toset /\ c e. B /\ a e. B ) -> ( c .< a <-> -. a .<_ c ) )
34 30 31 32 33 syl3anc 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( c .< a <-> -. a .<_ c ) )
35 34 con2bid 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( a .<_ c <-> -. c .< a ) )
36 29 35 imbi12d 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( ( A. b e. A b .<_ c -> a .<_ c ) <-> ( -. E. d e. A c .< d -> -. c .< a ) ) )
37 con34b 
 |-  ( ( c .< a -> E. d e. A c .< d ) <-> ( -. E. d e. A c .< d -> -. c .< a ) )
38 36 37 bitr4di 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( ( A. b e. A b .<_ c -> a .<_ c ) <-> ( c .< a -> E. d e. A c .< d ) ) )
39 38 ralbidva 
 |-  ( ( ph /\ a e. B ) -> ( A. c e. B ( A. b e. A b .<_ c -> a .<_ c ) <-> A. c e. B ( c .< a -> E. d e. A c .< d ) ) )
40 breq1 
 |-  ( b = c -> ( b .< a <-> c .< a ) )
41 breq1 
 |-  ( b = c -> ( b .< d <-> c .< d ) )
42 41 rexbidv 
 |-  ( b = c -> ( E. d e. A b .< d <-> E. d e. A c .< d ) )
43 40 42 imbi12d 
 |-  ( b = c -> ( ( b .< a -> E. d e. A b .< d ) <-> ( c .< a -> E. d e. A c .< d ) ) )
44 43 cbvralvw 
 |-  ( A. b e. B ( b .< a -> E. d e. A b .< d ) <-> A. c e. B ( c .< a -> E. d e. A c .< d ) )
45 39 44 bitr4di 
 |-  ( ( ph /\ a e. B ) -> ( A. c e. B ( A. b e. A b .<_ c -> a .<_ c ) <-> A. b e. B ( b .< a -> E. d e. A b .< d ) ) )
46 13 45 anbi12d 
 |-  ( ( ph /\ a e. B ) -> ( ( A. b e. A b .<_ a /\ A. c e. B ( A. b e. A b .<_ c -> a .<_ c ) ) <-> ( A. b e. A -. a .< b /\ A. b e. B ( b .< a -> E. d e. A b .< d ) ) ) )