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

Theorem ltsopr 7368
Description: Positive real 'less than' is a weak linear order (in the sense of df-iso 4187). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
Assertion
Ref Expression
ltsopr  |-  <P  Or  P.

Proof of Theorem ltsopr
Dummy variables  r  q  s  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltpopr 7367 . 2  |-  <P  Po  P.
2 ltdfpr 7278 . . . . 5  |-  ( ( x  e.  P.  /\  y  e.  P. )  ->  ( x  <P  y  <->  E. q  e.  Q.  (
q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y
) ) ) )
323adant3 984 . . . 4  |-  ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  ->  (
x  <P  y  <->  E. q  e.  Q.  ( q  e.  ( 2nd `  x
)  /\  q  e.  ( 1st `  y ) ) ) )
4 prop 7247 . . . . . . . . . . . 12  |-  ( x  e.  P.  ->  <. ( 1st `  x ) ,  ( 2nd `  x
) >.  e.  P. )
5 prnminu 7261 . . . . . . . . . . . 12  |-  ( (
<. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  P.  /\  q  e.  ( 2nd `  x ) )  ->  E. r  e.  ( 2nd `  x ) r 
<Q  q )
64, 5sylan 279 . . . . . . . . . . 11  |-  ( ( x  e.  P.  /\  q  e.  ( 2nd `  x ) )  ->  E. r  e.  ( 2nd `  x ) r 
<Q  q )
7 prop 7247 . . . . . . . . . . . 12  |-  ( y  e.  P.  ->  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  e.  P. )
8 prnmaxl 7260 . . . . . . . . . . . 12  |-  ( (
<. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  P.  /\  q  e.  ( 1st `  y ) )  ->  E. s  e.  ( 1st `  y ) q 
<Q  s )
97, 8sylan 279 . . . . . . . . . . 11  |-  ( ( y  e.  P.  /\  q  e.  ( 1st `  y ) )  ->  E. s  e.  ( 1st `  y ) q 
<Q  s )
106, 9anim12i 334 . . . . . . . . . 10  |-  ( ( ( x  e.  P.  /\  q  e.  ( 2nd `  x ) )  /\  ( y  e.  P.  /\  q  e.  ( 1st `  y ) ) )  ->  ( E. r  e.  ( 2nd `  x
) r  <Q  q  /\  E. s  e.  ( 1st `  y ) q  <Q  s )
)
1110an4s 560 . . . . . . . . 9  |-  ( ( ( x  e.  P.  /\  y  e.  P. )  /\  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) )  ->  ( E. r  e.  ( 2nd `  x ) r 
<Q  q  /\  E. s  e.  ( 1st `  y
) q  <Q  s
) )
12 reeanv 2575 . . . . . . . . 9  |-  ( E. r  e.  ( 2nd `  x ) E. s  e.  ( 1st `  y
) ( r  <Q 
q  /\  q  <Q  s )  <->  ( E. r  e.  ( 2nd `  x
) r  <Q  q  /\  E. s  e.  ( 1st `  y ) q  <Q  s )
)
1311, 12sylibr 133 . . . . . . . 8  |-  ( ( ( x  e.  P.  /\  y  e.  P. )  /\  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) )  ->  E. r  e.  ( 2nd `  x
) E. s  e.  ( 1st `  y
) ( r  <Q 
q  /\  q  <Q  s ) )
14133adantl3 1122 . . . . . . 7  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) )  ->  E. r  e.  ( 2nd `  x
) E. s  e.  ( 1st `  y
) ( r  <Q 
q  /\  q  <Q  s ) )
15 ltsonq 7170 . . . . . . . . . . . . 13  |-  <Q  Or  Q.
16 ltrelnq 7137 . . . . . . . . . . . . 13  |-  <Q  C_  ( Q.  X.  Q. )
1715, 16sotri 4902 . . . . . . . . . . . 12  |-  ( ( r  <Q  q  /\  q  <Q  s )  -> 
r  <Q  s )
1817adantl 273 . . . . . . . . . . 11  |-  ( ( ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e. 
P. )  /\  (
q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y
) ) )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  /\  (
r  <Q  q  /\  q  <Q  s ) )  -> 
r  <Q  s )
19 prop 7247 . . . . . . . . . . . . . . . 16  |-  ( z  e.  P.  ->  <. ( 1st `  z ) ,  ( 2nd `  z
) >.  e.  P. )
20 prloc 7263 . . . . . . . . . . . . . . . 16  |-  ( (
<. ( 1st `  z
) ,  ( 2nd `  z ) >.  e.  P.  /\  r  <Q  s )  ->  ( r  e.  ( 1st `  z )  \/  s  e.  ( 2nd `  z ) ) )
2119, 20sylan 279 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  P.  /\  r  <Q  s )  -> 
( r  e.  ( 1st `  z )  \/  s  e.  ( 2nd `  z ) ) )
22213ad2antl3 1128 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  r  <Q  s )  ->  ( r  e.  ( 1st `  z
)  \/  s  e.  ( 2nd `  z
) ) )
2322ex 114 . . . . . . . . . . . . 13  |-  ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  ->  (
r  <Q  s  ->  (
r  e.  ( 1st `  z )  \/  s  e.  ( 2nd `  z
) ) ) )
2423adantr 272 . . . . . . . . . . . 12  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) )  ->  (
r  <Q  s  ->  (
r  e.  ( 1st `  z )  \/  s  e.  ( 2nd `  z
) ) ) )
2524ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e. 
P. )  /\  (
q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y
) ) )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  /\  (
r  <Q  q  /\  q  <Q  s ) )  -> 
( r  <Q  s  ->  ( r  e.  ( 1st `  z )  \/  s  e.  ( 2nd `  z ) ) ) )
2618, 25mpd 13 . . . . . . . . . 10  |-  ( ( ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e. 
P. )  /\  (
q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y
) ) )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  /\  (
r  <Q  q  /\  q  <Q  s ) )  -> 
( r  e.  ( 1st `  z )  \/  s  e.  ( 2nd `  z ) ) )
27 elprnqu 7254 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
<. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  P.  /\  r  e.  ( 2nd `  x ) )  -> 
r  e.  Q. )
284, 27sylan 279 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  P.  /\  r  e.  ( 2nd `  x ) )  -> 
r  e.  Q. )
29 ax-ia3 107 . . . . . . . . . . . . . . . . . . . . 21  |-  ( r  e.  ( 2nd `  x
)  ->  ( r  e.  ( 1st `  z
)  ->  ( r  e.  ( 2nd `  x
)  /\  r  e.  ( 1st `  z ) ) ) )
3029adantl 273 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  P.  /\  r  e.  ( 2nd `  x ) )  -> 
( r  e.  ( 1st `  z )  ->  ( r  e.  ( 2nd `  x
)  /\  r  e.  ( 1st `  z ) ) ) )
31 19.8a 1552 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( r  e.  Q.  /\  ( r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z ) ) )  ->  E. r
( r  e.  Q.  /\  ( r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z ) ) ) )
3228, 30, 31syl6an 1393 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  P.  /\  r  e.  ( 2nd `  x ) )  -> 
( r  e.  ( 1st `  z )  ->  E. r ( r  e.  Q.  /\  (
r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z
) ) ) ) )
33323ad2antl1 1126 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  r  e.  ( 2nd `  x ) )  ->  ( r  e.  ( 1st `  z
)  ->  E. r
( r  e.  Q.  /\  ( r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z ) ) ) ) )
3433imp 123 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  r  e.  ( 2nd `  x ) )  /\  r  e.  ( 1st `  z
) )  ->  E. r
( r  e.  Q.  /\  ( r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z ) ) ) )
35 df-rex 2397 . . . . . . . . . . . . . . . . 17  |-  ( E. r  e.  Q.  (
r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z
) )  <->  E. r
( r  e.  Q.  /\  ( r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z ) ) ) )
3634, 35sylibr 133 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  r  e.  ( 2nd `  x ) )  /\  r  e.  ( 1st `  z
) )  ->  E. r  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  r  e.  ( 1st `  z ) ) )
37 ltdfpr 7278 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  P.  /\  z  e.  P. )  ->  ( x  <P  z  <->  E. r  e.  Q.  (
r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z
) ) ) )
3837biimprd 157 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  P.  /\  z  e.  P. )  ->  ( E. r  e. 
Q.  ( r  e.  ( 2nd `  x
)  /\  r  e.  ( 1st `  z ) )  ->  x  <P  z ) )
39383adant2 983 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  ->  ( E. r  e.  Q.  ( r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z ) )  ->  x  <P  z ) )
4039ad2antrr 477 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  r  e.  ( 2nd `  x ) )  /\  r  e.  ( 1st `  z
) )  ->  ( E. r  e.  Q.  ( r  e.  ( 2nd `  x )  /\  r  e.  ( 1st `  z ) )  ->  x  <P  z ) )
4136, 40mpd 13 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  r  e.  ( 2nd `  x ) )  /\  r  e.  ( 1st `  z
) )  ->  x  <P  z )
4241ex 114 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  r  e.  ( 2nd `  x ) )  ->  ( r  e.  ( 1st `  z
)  ->  x  <P  z ) )
4342adantrr 468 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  ->  (
r  e.  ( 1st `  z )  ->  x  <P  z ) )
44 elprnql 7253 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
<. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  P.  /\  s  e.  ( 1st `  y ) )  -> 
s  e.  Q. )
457, 44sylan 279 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  P.  /\  s  e.  ( 1st `  y ) )  -> 
s  e.  Q. )
46 pm3.21 262 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( 1st `  y
)  ->  ( s  e.  ( 2nd `  z
)  ->  ( s  e.  ( 2nd `  z
)  /\  s  e.  ( 1st `  y ) ) ) )
4746adantl 273 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  P.  /\  s  e.  ( 1st `  y ) )  -> 
( s  e.  ( 2nd `  z )  ->  ( s  e.  ( 2nd `  z
)  /\  s  e.  ( 1st `  y ) ) ) )
48 19.8a 1552 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  Q.  /\  ( s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y ) ) )  ->  E. s
( s  e.  Q.  /\  ( s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y ) ) ) )
4945, 47, 48syl6an 1393 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  P.  /\  s  e.  ( 1st `  y ) )  -> 
( s  e.  ( 2nd `  z )  ->  E. s ( s  e.  Q.  /\  (
s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y
) ) ) ) )
50493ad2antl2 1127 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  s  e.  ( 1st `  y ) )  ->  ( s  e.  ( 2nd `  z
)  ->  E. s
( s  e.  Q.  /\  ( s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y ) ) ) ) )
5150imp 123 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  s  e.  ( 1st `  y ) )  /\  s  e.  ( 2nd `  z
) )  ->  E. s
( s  e.  Q.  /\  ( s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y ) ) ) )
52 df-rex 2397 . . . . . . . . . . . . . . . . 17  |-  ( E. s  e.  Q.  (
s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y
) )  <->  E. s
( s  e.  Q.  /\  ( s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y ) ) ) )
5351, 52sylibr 133 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  s  e.  ( 1st `  y ) )  /\  s  e.  ( 2nd `  z
) )  ->  E. s  e.  Q.  ( s  e.  ( 2nd `  z
)  /\  s  e.  ( 1st `  y ) ) )
54 ltdfpr 7278 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  P.  /\  y  e.  P. )  ->  ( z  <P  y  <->  E. s  e.  Q.  (
s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y
) ) ) )
5554biimprd 157 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  P.  /\  y  e.  P. )  ->  ( E. s  e. 
Q.  ( s  e.  ( 2nd `  z
)  /\  s  e.  ( 1st `  y ) )  ->  z  <P  y ) )
5655ancoms 266 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  P.  /\  z  e.  P. )  ->  ( E. s  e. 
Q.  ( s  e.  ( 2nd `  z
)  /\  s  e.  ( 1st `  y ) )  ->  z  <P  y ) )
57563adant1 982 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  ->  ( E. s  e.  Q.  ( s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y ) )  ->  z  <P  y ) )
5857ad2antrr 477 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  s  e.  ( 1st `  y ) )  /\  s  e.  ( 2nd `  z
) )  ->  ( E. s  e.  Q.  ( s  e.  ( 2nd `  z )  /\  s  e.  ( 1st `  y ) )  ->  z  <P  y ) )
5953, 58mpd 13 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  s  e.  ( 1st `  y ) )  /\  s  e.  ( 2nd `  z
) )  ->  z  <P  y )
6059ex 114 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  s  e.  ( 1st `  y ) )  ->  ( s  e.  ( 2nd `  z
)  ->  z  <P  y ) )
6160adantrl 467 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  ->  (
s  e.  ( 2nd `  z )  ->  z  <P  y ) )
6243, 61orim12d 758 . . . . . . . . . . . 12  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  ->  (
( r  e.  ( 1st `  z )  \/  s  e.  ( 2nd `  z ) )  ->  ( x  <P  z  \/  z  <P 
y ) ) )
6362adantlr 466 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( q  e.  ( 2nd `  x
)  /\  q  e.  ( 1st `  y ) ) )  /\  (
r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y
) ) )  -> 
( ( r  e.  ( 1st `  z
)  \/  s  e.  ( 2nd `  z
) )  ->  (
x  <P  z  \/  z  <P  y ) ) )
6463adantr 272 . . . . . . . . . 10  |-  ( ( ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e. 
P. )  /\  (
q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y
) ) )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  /\  (
r  <Q  q  /\  q  <Q  s ) )  -> 
( ( r  e.  ( 1st `  z
)  \/  s  e.  ( 2nd `  z
) )  ->  (
x  <P  z  \/  z  <P  y ) ) )
6526, 64mpd 13 . . . . . . . . 9  |-  ( ( ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e. 
P. )  /\  (
q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y
) ) )  /\  ( r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y ) ) )  /\  (
r  <Q  q  /\  q  <Q  s ) )  -> 
( x  <P  z  \/  z  <P  y ) )
6665ex 114 . . . . . . . 8  |-  ( ( ( ( x  e. 
P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( q  e.  ( 2nd `  x
)  /\  q  e.  ( 1st `  y ) ) )  /\  (
r  e.  ( 2nd `  x )  /\  s  e.  ( 1st `  y
) ) )  -> 
( ( r  <Q 
q  /\  q  <Q  s )  ->  ( x  <P  z  \/  z  <P 
y ) ) )
6766rexlimdvva 2532 . . . . . . 7  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) )  ->  ( E. r  e.  ( 2nd `  x ) E. s  e.  ( 1st `  y ) ( r 
<Q  q  /\  q  <Q  s )  ->  (
x  <P  z  \/  z  <P  y ) ) )
6814, 67mpd 13 . . . . . 6  |-  ( ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  /\  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) )  ->  (
x  <P  z  \/  z  <P  y ) )
6968ex 114 . . . . 5  |-  ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  ->  (
( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) )  ->  ( x  <P  z  \/  z  <P 
y ) ) )
7069rexlimdvw 2528 . . . 4  |-  ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  ->  ( E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) )  ->  ( x  <P  z  \/  z  <P 
y ) ) )
713, 70sylbid 149 . . 3  |-  ( ( x  e.  P.  /\  y  e.  P.  /\  z  e.  P. )  ->  (
x  <P  y  ->  (
x  <P  z  \/  z  <P  y ) ) )
7271rgen3 2494 . 2  |-  A. x  e.  P.  A. y  e. 
P.  A. z  e.  P.  ( x  <P  y  -> 
( x  <P  z  \/  z  <P  y ) )
73 df-iso 4187 . 2  |-  (  <P  Or  P.  <->  (  <P  Po  P.  /\ 
A. x  e.  P.  A. y  e.  P.  A. z  e.  P.  (
x  <P  y  ->  (
x  <P  z  \/  z  <P  y ) ) ) )
741, 72, 73mpbir2an 909 1  |-  <P  Or  P.
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680    /\ w3a 945   E.wex 1451    e. wcel 1463   A.wral 2391   E.wrex 2392   <.cop 3498   class class class wbr 3897    Po wpo 4184    Or wor 4185   ` cfv 5091   1stc1st 6002   2ndc2nd 6003   Q.cnq 7052    <Q cltq 7057   P.cnp 7063    <P cltp 7067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-reu 2398  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-eprel 4179  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-oadd 6283  df-omul 6284  df-er 6395  df-ec 6397  df-qs 6401  df-ni 7076  df-mi 7078  df-lti 7079  df-enq 7119  df-nqqs 7120  df-ltnqqs 7125  df-inp 7238  df-iltp 7242
This theorem is referenced by:  prplnqu  7392  addextpr  7393  caucvgprprlemk  7455  caucvgprprlemnkltj  7461  caucvgprprlemnkeqj  7462  caucvgprprlemnjltk  7463  caucvgprprlemnbj  7465  caucvgprprlemml  7466  caucvgprprlemlol  7470  caucvgprprlemupu  7472  caucvgprprlemloc  7475  caucvgprprlemaddq  7480  suplocexprlemmu  7490  lttrsr  7534  ltposr  7535  ltsosr  7536  archsr  7554
  Copyright terms: Public domain W3C validator