This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tosglblem

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

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

Proof

Step Hyp Ref Expression
1 tosglb.b 
 |-  B = ( Base ` K )
2 tosglb.l 
 |-  .< = ( lt ` K )
3 tosglb.1 
 |-  ( ph -> K e. Toset )
4 tosglb.2 
 |-  ( ph -> A C_ B )
5 tosglb.e 
 |-  .<_ = ( le ` K )
6 3 ad2antrr 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> K e. Toset )
7 4 adantr 
 |-  ( ( ph /\ a e. B ) -> A C_ B )
8 7 sselda 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> b e. B )
9 simplr 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> a e. B )
10 1 5 2 tltnle 
 |-  ( ( K e. Toset /\ b e. B /\ a e. B ) -> ( b .< a <-> -. a .<_ b ) )
11 6 8 9 10 syl3anc 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> ( b .< a <-> -. a .<_ b ) )
12 11 con2bid 
 |-  ( ( ( ph /\ a e. B ) /\ b e. A ) -> ( a .<_ b <-> -. b .< a ) )
13 12 ralbidva 
 |-  ( ( ph /\ a e. B ) -> ( A. b e. A a .<_ b <-> A. b e. A -. b .< a ) )
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 /\ b e. B /\ c e. B ) -> ( b .< c <-> -. c .<_ b ) )
18 3 17 syl3an1 
 |-  ( ( ph /\ b e. B /\ c e. B ) -> ( b .< c <-> -. c .<_ b ) )
19 18 3com23 
 |-  ( ( ph /\ c e. B /\ b e. B ) -> ( b .< c <-> -. c .<_ b ) )
20 19 3expa 
 |-  ( ( ( ph /\ c e. B ) /\ b e. B ) -> ( b .< c <-> -. c .<_ b ) )
21 20 con2bid 
 |-  ( ( ( ph /\ c e. B ) /\ b e. B ) -> ( c .<_ b <-> -. b .< c ) )
22 16 21 syldan 
 |-  ( ( ( ph /\ c e. B ) /\ b e. A ) -> ( c .<_ b <-> -. b .< c ) )
23 22 ralbidva 
 |-  ( ( ph /\ c e. B ) -> ( A. b e. A c .<_ b <-> A. b e. A -. b .< c ) )
24 breq1 
 |-  ( b = d -> ( b .< c <-> d .< c ) )
25 24 notbid 
 |-  ( b = d -> ( -. b .< c <-> -. d .< c ) )
26 25 cbvralvw 
 |-  ( A. b e. A -. b .< c <-> A. d e. A -. d .< c )
27 ralnex 
 |-  ( A. d e. A -. d .< c <-> -. E. d e. A d .< c )
28 26 27 bitri 
 |-  ( A. b e. A -. b .< c <-> -. E. d e. A d .< c )
29 23 28 bitrdi 
 |-  ( ( ph /\ c e. B ) -> ( A. b e. A c .<_ b <-> -. E. d e. A d .< c ) )
30 29 adantlr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( A. b e. A c .<_ b <-> -. E. d e. A d .< c ) )
31 3 ad2antrr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> K e. Toset )
32 simplr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> a e. B )
33 simpr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> c e. B )
34 1 5 2 tltnle 
 |-  ( ( K e. Toset /\ a e. B /\ c e. B ) -> ( a .< c <-> -. c .<_ a ) )
35 31 32 33 34 syl3anc 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( a .< c <-> -. c .<_ a ) )
36 35 con2bid 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( c .<_ a <-> -. a .< c ) )
37 30 36 imbi12d 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( ( A. b e. A c .<_ b -> c .<_ a ) <-> ( -. E. d e. A d .< c -> -. a .< c ) ) )
38 con34b 
 |-  ( ( a .< c -> E. d e. A d .< c ) <-> ( -. E. d e. A d .< c -> -. a .< c ) )
39 37 38 bitr4di 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( ( A. b e. A c .<_ b -> c .<_ a ) <-> ( a .< c -> E. d e. A d .< c ) ) )
40 39 ralbidva 
 |-  ( ( ph /\ a e. B ) -> ( A. c e. B ( A. b e. A c .<_ b -> c .<_ a ) <-> A. c e. B ( a .< c -> E. d e. A d .< c ) ) )
41 breq2 
 |-  ( b = c -> ( a .< b <-> a .< c ) )
42 breq2 
 |-  ( b = c -> ( d .< b <-> d .< c ) )
43 42 rexbidv 
 |-  ( b = c -> ( E. d e. A d .< b <-> E. d e. A d .< c ) )
44 41 43 imbi12d 
 |-  ( b = c -> ( ( a .< b -> E. d e. A d .< b ) <-> ( a .< c -> E. d e. A d .< c ) ) )
45 44 cbvralvw 
 |-  ( A. b e. B ( a .< b -> E. d e. A d .< b ) <-> A. c e. B ( a .< c -> E. d e. A d .< c ) )
46 40 45 bitr4di 
 |-  ( ( ph /\ a e. B ) -> ( A. c e. B ( A. b e. A c .<_ b -> c .<_ a ) <-> A. b e. B ( a .< b -> E. d e. A d .< b ) ) )
47 13 46 anbi12d 
 |-  ( ( ph /\ a e. B ) -> ( ( A. b e. A a .<_ b /\ A. c e. B ( A. b e. A c .<_ b -> c .<_ a ) ) <-> ( A. b e. A -. b .< a /\ A. b e. B ( a .< b -> E. d e. A d .< b ) ) ) )
48 vex 
 |-  a e. _V
49 vex 
 |-  b e. _V
50 48 49 brcnv 
 |-  ( a `' .< b <-> b .< a )
51 50 notbii 
 |-  ( -. a `' .< b <-> -. b .< a )
52 51 ralbii 
 |-  ( A. b e. A -. a `' .< b <-> A. b e. A -. b .< a )
53 49 48 brcnv 
 |-  ( b `' .< a <-> a .< b )
54 vex 
 |-  d e. _V
55 49 54 brcnv 
 |-  ( b `' .< d <-> d .< b )
56 55 rexbii 
 |-  ( E. d e. A b `' .< d <-> E. d e. A d .< b )
57 53 56 imbi12i 
 |-  ( ( b `' .< a -> E. d e. A b `' .< d ) <-> ( a .< b -> E. d e. A d .< b ) )
58 57 ralbii 
 |-  ( A. b e. B ( b `' .< a -> E. d e. A b `' .< d ) <-> A. b e. B ( a .< b -> E. d e. A d .< b ) )
59 52 58 anbi12i 
 |-  ( ( A. b e. A -. a `' .< b /\ A. b e. B ( b `' .< a -> E. d e. A b `' .< d ) ) <-> ( A. b e. A -. b .< a /\ A. b e. B ( a .< b -> E. d e. A d .< b ) ) )
60 47 59 bitr4di 
 |-  ( ( ph /\ a e. B ) -> ( ( A. b e. A a .<_ b /\ A. c e. B ( A. b e. A c .<_ b -> c .<_ a ) ) <-> ( A. b e. A -. a `' .< b /\ A. b e. B ( b `' .< a -> E. d e. A b `' .< d ) ) ) )