ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltdfpr Unicode version

Theorem ltdfpr 6810
Description: More convenient form of df-iltp 6774. (Contributed by Jim Kingdon, 15-Dec-2019.)
Assertion
Ref Expression
ltdfpr  |-  ( ( A  e.  P.  /\  B  e.  P. )  ->  ( A  <P  B  <->  E. q  e.  Q.  ( q  e.  ( 2nd `  A
)  /\  q  e.  ( 1st `  B ) ) ) )
Distinct variable groups:    A, q    B, q

Proof of Theorem ltdfpr
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 3806 . . 3  |-  ( A 
<P  B  <->  <. A ,  B >.  e.  <P  )
2 df-iltp 6774 . . . 4  |-  <P  =  { <. x ,  y
>.  |  ( (
x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
32eleq2i 2149 . . 3  |-  ( <. A ,  B >.  e. 
<P 
<-> 
<. A ,  B >.  e. 
{ <. x ,  y
>.  |  ( (
x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) } )
41, 3bitri 182 . 2  |-  ( A 
<P  B  <->  <. A ,  B >.  e.  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) } )
5 simpl 107 . . . . . . 7  |-  ( ( x  =  A  /\  y  =  B )  ->  x  =  A )
65fveq2d 5233 . . . . . 6  |-  ( ( x  =  A  /\  y  =  B )  ->  ( 2nd `  x
)  =  ( 2nd `  A ) )
76eleq2d 2152 . . . . 5  |-  ( ( x  =  A  /\  y  =  B )  ->  ( q  e.  ( 2nd `  x )  <-> 
q  e.  ( 2nd `  A ) ) )
8 simpr 108 . . . . . . 7  |-  ( ( x  =  A  /\  y  =  B )  ->  y  =  B )
98fveq2d 5233 . . . . . 6  |-  ( ( x  =  A  /\  y  =  B )  ->  ( 1st `  y
)  =  ( 1st `  B ) )
109eleq2d 2152 . . . . 5  |-  ( ( x  =  A  /\  y  =  B )  ->  ( q  e.  ( 1st `  y )  <-> 
q  e.  ( 1st `  B ) ) )
117, 10anbi12d 457 . . . 4  |-  ( ( x  =  A  /\  y  =  B )  ->  ( ( q  e.  ( 2nd `  x
)  /\  q  e.  ( 1st `  y ) )  <->  ( q  e.  ( 2nd `  A
)  /\  q  e.  ( 1st `  B ) ) ) )
1211rexbidv 2374 . . 3  |-  ( ( x  =  A  /\  y  =  B )  ->  ( E. q  e. 
Q.  ( q  e.  ( 2nd `  x
)  /\  q  e.  ( 1st `  y ) )  <->  E. q  e.  Q.  ( q  e.  ( 2nd `  A )  /\  q  e.  ( 1st `  B ) ) ) )
1312opelopab2a 4048 . 2  |-  ( ( A  e.  P.  /\  B  e.  P. )  ->  ( <. A ,  B >.  e.  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }  <->  E. q  e.  Q.  ( q  e.  ( 2nd `  A
)  /\  q  e.  ( 1st `  B ) ) ) )
144, 13syl5bb 190 1  |-  ( ( A  e.  P.  /\  B  e.  P. )  ->  ( A  <P  B  <->  E. q  e.  Q.  ( q  e.  ( 2nd `  A
)  /\  q  e.  ( 1st `  B ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285    e. wcel 1434   E.wrex 2354   <.cop 3419   class class class wbr 3805   {copab 3858   ` cfv 4952   1stc1st 5816   2ndc2nd 5817   Q.cnq 6584   P.cnp 6595    <P cltp 6599
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2612  df-un 2986  df-in 2988  df-ss 2995  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-opab 3860  df-iota 4917  df-fv 4960  df-iltp 6774
This theorem is referenced by:  nqprl  6855  nqpru  6856  ltprordil  6893  ltnqpr  6897  ltnqpri  6898  ltpopr  6899  ltsopr  6900  ltaddpr  6901  ltexprlemm  6904  ltexprlemopu  6907  ltexprlemru  6916  aptiprleml  6943  aptiprlemu  6944  archpr  6947  cauappcvgprlem2  6964  caucvgprlem2  6984  caucvgprprlemopu  7003  caucvgprprlemexbt  7010  caucvgprprlem2  7014
  Copyright terms: Public domain W3C validator