Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tosglblem Structured version   Unicode version

Theorem tosglblem 28268
Description: Lemma for tosglb 28269 and xrsclat 28279. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
Hypotheses
Ref Expression
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
Ref Expression
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 ) ) ) )
Distinct variable groups:    a, b,
c, d,  .<    A, a, b, c, d    B, a, b, c, d    K, a, b, c    ph, a,
b, c
Allowed substitution hints:    ph( d)    K( d)   
.<_ ( a, b, c, d)

Proof of Theorem tosglblem
StepHypRef Expression
1 tosglb.1 . . . . . . 7  |-  ( ph  ->  K  e. Toset )
21ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  a  e.  B )  /\  b  e.  A )  ->  K  e. Toset )
3 tosglb.2 . . . . . . . 8  |-  ( ph  ->  A  C_  B )
43adantr 466 . . . . . . 7  |-  ( (
ph  /\  a  e.  B )  ->  A  C_  B )
54sselda 3470 . . . . . 6  |-  ( ( ( ph  /\  a  e.  B )  /\  b  e.  A )  ->  b  e.  B )
6 simplr 760 . . . . . 6  |-  ( ( ( ph  /\  a  e.  B )  /\  b  e.  A )  ->  a  e.  B )
7 tosglb.b . . . . . . 7  |-  B  =  ( Base `  K
)
8 tosglb.e . . . . . . 7  |-  .<_  =  ( le `  K )
9 tosglb.l . . . . . . 7  |-  .<  =  ( lt `  K )
107, 8, 9tltnle 28261 . . . . . 6  |-  ( ( K  e. Toset  /\  b  e.  B  /\  a  e.  B )  ->  (
b  .<  a  <->  -.  a  .<_  b ) )
112, 5, 6, 10syl3anc 1264 . . . . 5  |-  ( ( ( ph  /\  a  e.  B )  /\  b  e.  A )  ->  (
b  .<  a  <->  -.  a  .<_  b ) )
1211con2bid 330 . . . 4  |-  ( ( ( ph  /\  a  e.  B )  /\  b  e.  A )  ->  (
a  .<_  b  <->  -.  b  .<  a ) )
1312ralbidva 2868 . . 3  |-  ( (
ph  /\  a  e.  B )  ->  ( A. b  e.  A  a  .<_  b  <->  A. b  e.  A  -.  b  .<  a ) )
143ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  B )  /\  b  e.  A )  ->  A  C_  B )
15 simpr 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  B )  /\  b  e.  A )  ->  b  e.  A )
1614, 15sseldd 3471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  B )  /\  b  e.  A )  ->  b  e.  B )
177, 8, 9tltnle 28261 . . . . . . . . . . . . . . 15  |-  ( ( K  e. Toset  /\  b  e.  B  /\  c  e.  B )  ->  (
b  .<  c  <->  -.  c  .<_  b ) )
181, 17syl3an1 1297 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B  /\  c  e.  B
)  ->  ( b  .<  c  <->  -.  c  .<_  b ) )
19183com23 1211 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  B  /\  b  e.  B
)  ->  ( b  .<  c  <->  -.  c  .<_  b ) )
20193expa 1205 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  B )  /\  b  e.  B )  ->  (
b  .<  c  <->  -.  c  .<_  b ) )
2120con2bid 330 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  B )  /\  b  e.  B )  ->  (
c  .<_  b  <->  -.  b  .<  c ) )
2216, 21syldan 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  B )  /\  b  e.  A )  ->  (
c  .<_  b  <->  -.  b  .<  c ) )
2322ralbidva 2868 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  B )  ->  ( A. b  e.  A  c  .<_  b  <->  A. b  e.  A  -.  b  .<  c ) )
24 breq1 4429 . . . . . . . . . . . 12  |-  ( b  =  d  ->  (
b  .<  c  <->  d  .<  c ) )
2524notbid 295 . . . . . . . . . . 11  |-  ( b  =  d  ->  ( -.  b  .<  c  <->  -.  d  .<  c ) )
2625cbvralv 3062 . . . . . . . . . 10  |-  ( A. b  e.  A  -.  b  .<  c  <->  A. d  e.  A  -.  d  .<  c )
27 ralnex 2878 . . . . . . . . . 10  |-  ( A. d  e.  A  -.  d  .<  c  <->  -.  E. d  e.  A  d  .<  c )
2826, 27bitri 252 . . . . . . . . 9  |-  ( A. b  e.  A  -.  b  .<  c  <->  -.  E. d  e.  A  d  .<  c )
2923, 28syl6bb 264 . . . . . . . 8  |-  ( (
ph  /\  c  e.  B )  ->  ( A. b  e.  A  c  .<_  b  <->  -.  E. d  e.  A  d  .<  c ) )
3029adantlr 719 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  B )  /\  c  e.  B )  ->  ( A. b  e.  A  c  .<_  b  <->  -.  E. d  e.  A  d  .<  c ) )
311ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  B )  /\  c  e.  B )  ->  K  e. Toset )
32 simplr 760 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  B )  /\  c  e.  B )  ->  a  e.  B )
33 simpr 462 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  B )  /\  c  e.  B )  ->  c  e.  B )
347, 8, 9tltnle 28261 . . . . . . . . 9  |-  ( ( K  e. Toset  /\  a  e.  B  /\  c  e.  B )  ->  (
a  .<  c  <->  -.  c  .<_  a ) )
3531, 32, 33, 34syl3anc 1264 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  B )  /\  c  e.  B )  ->  (
a  .<  c  <->  -.  c  .<_  a ) )
3635con2bid 330 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  B )  /\  c  e.  B )  ->  (
c  .<_  a  <->  -.  a  .<  c ) )
3730, 36imbi12d 321 . . . . . 6  |-  ( ( ( 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 293 . . . . . 6  |-  ( ( a  .<  c  ->  E. d  e.  A  d 
.<  c )  <->  ( -.  E. d  e.  A  d 
.<  c  ->  -.  a  .<  c ) )
3937, 38syl6bbr 266 . . . . 5  |-  ( ( ( ph  /\  a  e.  B )  /\  c  e.  B )  ->  (
( A. b  e.  A  c  .<_  b  -> 
c  .<_  a )  <->  ( a  .<  c  ->  E. d  e.  A  d  .<  c ) ) )
4039ralbidva 2868 . . . 4  |-  ( (
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 4430 . . . . . 6  |-  ( b  =  c  ->  (
a  .<  b  <->  a  .<  c ) )
42 breq2 4430 . . . . . . 7  |-  ( b  =  c  ->  (
d  .<  b  <->  d  .<  c ) )
4342rexbidv 2946 . . . . . 6  |-  ( b  =  c  ->  ( E. d  e.  A  d  .<  b  <->  E. d  e.  A  d  .<  c ) )
4441, 43imbi12d 321 . . . . 5  |-  ( b  =  c  ->  (
( a  .<  b  ->  E. d  e.  A  d  .<  b )  <->  ( a  .<  c  ->  E. d  e.  A  d  .<  c ) ) )
4544cbvralv 3062 . . . 4  |-  ( A. b  e.  B  (
a  .<  b  ->  E. d  e.  A  d  .<  b )  <->  A. c  e.  B  ( a  .<  c  ->  E. d  e.  A  d  .<  c ) )
4640, 45syl6bbr 266 . . 3  |-  ( (
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 ) ) )
4713, 46anbi12d 715 . 2  |-  ( (
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 3090 . . . . . 6  |-  a  e. 
_V
49 vex 3090 . . . . . 6  |-  b  e. 
_V
5048, 49brcnv 5037 . . . . 5  |-  ( a `'  .<  b  <->  b  .<  a )
5150notbii 297 . . . 4  |-  ( -.  a `'  .<  b  <->  -.  b  .<  a )
5251ralbii 2863 . . 3  |-  ( A. b  e.  A  -.  a `'  .<  b  <->  A. b  e.  A  -.  b  .<  a )
5349, 48brcnv 5037 . . . . 5  |-  ( b `'  .<  a  <->  a  .<  b )
54 vex 3090 . . . . . . 7  |-  d  e. 
_V
5549, 54brcnv 5037 . . . . . 6  |-  ( b `'  .<  d  <->  d  .<  b )
5655rexbii 2934 . . . . 5  |-  ( E. d  e.  A  b `'  .<  d  <->  E. d  e.  A  d  .<  b )
5753, 56imbi12i 327 . . . 4  |-  ( ( b `'  .<  a  ->  E. d  e.  A  b `'  .<  d )  <-> 
( a  .<  b  ->  E. d  e.  A  d  .<  b ) )
5857ralbii 2863 . . 3  |-  ( A. b  e.  B  (
b `'  .<  a  ->  E. d  e.  A  b `'  .<  d )  <->  A. b  e.  B  ( a  .<  b  ->  E. d  e.  A  d  .<  b ) )
5952, 58anbi12i 701 . 2  |-  ( ( 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 ) ) )
6047, 59syl6bbr 266 1  |-  ( (
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 ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870   A.wral 2782   E.wrex 2783    C_ wss 3442   class class class wbr 4426   `'ccnv 4853   ` cfv 5601   Basecbs 15084   lecple 15159   ltcplt 16137  Tosetctos 16230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-iota 5565  df-fun 5603  df-fv 5609  df-preset 16124  df-poset 16142  df-plt 16155  df-toset 16231
This theorem is referenced by:  tosglb  28269  xrsclat  28279
  Copyright terms: Public domain W3C validator