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.

Step	Hyp	Ref	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 ) ) ) }
3	2	eleq2i 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 ) ) ) } )
4	1, 3	bitri 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 )
6	5	fveq2d 5233	. . . . . 6 |- ( ( x = A /\ y = B ) -> ( 2nd ` x ) = ( 2nd ` A ) )
7	6	eleq2d 2152	. . . . 5 |- ( ( x = A /\ y = B ) -> ( q e. ( 2nd ` x ) <-> q e. ( 2nd ` A ) ) )
8		simpr 108	. . . . . . 7 |- ( ( x = A /\ y = B ) -> y = B )
9	8	fveq2d 5233	. . . . . 6 |- ( ( x = A /\ y = B ) -> ( 1st ` y ) = ( 1st ` B ) )
10	9	eleq2d 2152	. . . . 5 |- ( ( x = A /\ y = B ) -> ( q e. ( 1st ` y ) <-> q e. ( 1st ` B ) ) )
11	7, 10	anbi12d 457	. . . 4 |- ( ( x = A /\ y = B ) -> ( ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) <-> ( q e. ( 2nd ` A ) /\ q e. ( 1st ` B ) ) ) )
12	11	rexbidv 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 ) ) ) )
13	12	opelopab2a 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 ) ) ) )
14	4, 13	syl5bb 190	1 |- ( ( A e. P. /\ B e. P. ) -> ( A <P B <-> E. q e. Q. ( q e. ( 2nd ` A ) /\ q e. ( 1st ` B ) ) ) )

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