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

Theorem xblss2ps 13537
Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 13540 for extended metrics, we have to assume the balls are a finite distance apart, or else  P will not even be in the infinity ball around  Q. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
Hypotheses
Ref Expression
xblss2ps.1  |-  ( ph  ->  D  e.  (PsMet `  X ) )
xblss2ps.2  |-  ( ph  ->  P  e.  X )
xblss2ps.3  |-  ( ph  ->  Q  e.  X )
xblss2ps.4  |-  ( ph  ->  R  e.  RR* )
xblss2ps.5  |-  ( ph  ->  S  e.  RR* )
xblss2ps.6  |-  ( ph  ->  ( P D Q )  e.  RR )
xblss2ps.7  |-  ( ph  ->  ( P D Q )  <_  ( S +e  -e R ) )
Assertion
Ref Expression
xblss2ps  |-  ( ph  ->  ( P ( ball `  D ) R ) 
C_  ( Q (
ball `  D ) S ) )

Proof of Theorem xblss2ps
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 xblss2ps.1 . . . . . 6  |-  ( ph  ->  D  e.  (PsMet `  X ) )
2 xblss2ps.2 . . . . . 6  |-  ( ph  ->  P  e.  X )
3 xblss2ps.4 . . . . . 6  |-  ( ph  ->  R  e.  RR* )
4 elblps 13523 . . . . . 6  |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  R  e. 
RR* )  ->  (
x  e.  ( P ( ball `  D
) R )  <->  ( x  e.  X  /\  ( P D x )  < 
R ) ) )
51, 2, 3, 4syl3anc 1238 . . . . 5  |-  ( ph  ->  ( x  e.  ( P ( ball `  D
) R )  <->  ( x  e.  X  /\  ( P D x )  < 
R ) ) )
65simprbda 383 . . . 4  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  x  e.  X
)
71adantr 276 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  D  e.  (PsMet `  X ) )
8 xblss2ps.3 . . . . . . . . 9  |-  ( ph  ->  Q  e.  X )
98adantr 276 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  Q  e.  X
)
10 psmetcl 13459 . . . . . . . 8  |-  ( ( D  e.  (PsMet `  X )  /\  Q  e.  X  /\  x  e.  X )  ->  ( Q D x )  e. 
RR* )
117, 9, 6, 10syl3anc 1238 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( Q D x )  e.  RR* )
1211adantr 276 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  ( Q D x )  e. 
RR* )
13 xblss2ps.6 . . . . . . . . . 10  |-  ( ph  ->  ( P D Q )  e.  RR )
1413adantr 276 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( P D Q )  e.  RR )
1514rexrd 7984 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( P D Q )  e.  RR* )
163adantr 276 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  R  e.  RR* )
1715, 16xaddcld 9858 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( ( P D Q ) +e R )  e. 
RR* )
1817adantr 276 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  (
( P D Q ) +e R )  e.  RR* )
19 xblss2ps.5 . . . . . . 7  |-  ( ph  ->  S  e.  RR* )
2019ad2antrr 488 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  S  e.  RR* )
212adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  P  e.  X
)
22 psmetcl 13459 . . . . . . . . . 10  |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  x  e.  X )  ->  ( P D x )  e. 
RR* )
237, 21, 6, 22syl3anc 1238 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( P D x )  e.  RR* )
2415, 23xaddcld 9858 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( ( P D Q ) +e ( P D x ) )  e. 
RR* )
25 psmettri2 13461 . . . . . . . . 9  |-  ( ( D  e.  (PsMet `  X )  /\  ( P  e.  X  /\  Q  e.  X  /\  x  e.  X )
)  ->  ( Q D x )  <_ 
( ( P D Q ) +e
( P D x ) ) )
267, 21, 9, 6, 25syl13anc 1240 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( Q D x )  <_  (
( P D Q ) +e ( P D x ) ) )
275simplbda 384 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( P D x )  <  R
)
28 xltadd2 9851 . . . . . . . . . 10  |-  ( ( ( P D x )  e.  RR*  /\  R  e.  RR*  /\  ( P D Q )  e.  RR )  ->  (
( P D x )  <  R  <->  ( ( P D Q ) +e ( P D x ) )  < 
( ( P D Q ) +e
R ) ) )
2923, 16, 14, 28syl3anc 1238 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( ( P D x )  < 
R  <->  ( ( P D Q ) +e ( P D x ) )  < 
( ( P D Q ) +e
R ) ) )
3027, 29mpbid 147 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( ( P D Q ) +e ( P D x ) )  < 
( ( P D Q ) +e
R ) )
3111, 24, 17, 26, 30xrlelttrd 9784 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( Q D x )  <  (
( P D Q ) +e R ) )
3231adantr 276 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  ( Q D x )  < 
( ( P D Q ) +e
R ) )
3319adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  S  e.  RR* )
3416xnegcld 9829 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  -e R  e. 
RR* )
3533, 34xaddcld 9858 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( S +e  -e R )  e.  RR* )
36 xblss2ps.7 . . . . . . . . . 10  |-  ( ph  ->  ( P D Q )  <_  ( S +e  -e R ) )
3736adantr 276 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( P D Q )  <_  ( S +e  -e
R ) )
38 xleadd1a 9847 . . . . . . . . 9  |-  ( ( ( ( P D Q )  e.  RR*  /\  ( S +e  -e R )  e. 
RR*  /\  R  e.  RR* )  /\  ( P D Q )  <_ 
( S +e  -e R ) )  ->  ( ( P D Q ) +e R )  <_ 
( ( S +e  -e R ) +e R ) )
3915, 35, 16, 37, 38syl31anc 1241 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( ( P D Q ) +e R )  <_ 
( ( S +e  -e R ) +e R ) )
4039adantr 276 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  (
( P D Q ) +e R )  <_  ( ( S +e  -e
R ) +e
R ) )
41 xnpcan 9846 . . . . . . . 8  |-  ( ( S  e.  RR*  /\  R  e.  RR )  ->  (
( S +e  -e R ) +e R )  =  S )
4233, 41sylan 283 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  (
( S +e  -e R ) +e R )  =  S )
4340, 42breqtrd 4026 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  (
( P D Q ) +e R )  <_  S )
4412, 18, 20, 32, 43xrltletrd 9785 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  e.  RR )  ->  ( Q D x )  < 
S )
4511adantr 276 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( Q D x )  e. 
RR* )
4613ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( P D Q )  e.  RR )
47 simpll 527 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ph )
48 simplr 528 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  x  e.  ( P ( ball `  D ) R ) )
49 simpr 110 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  R  = +oo )
5049oveq2d 5884 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( P ( ball `  D
) R )  =  ( P ( ball `  D ) +oo )
)
5148, 50eleqtrd 2256 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  x  e.  ( P ( ball `  D ) +oo )
)
52 xblpnfps 13531 . . . . . . . . . . . 12  |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X )  ->  (
x  e.  ( P ( ball `  D
) +oo )  <->  ( x  e.  X  /\  ( P D x )  e.  RR ) ) )
531, 2, 52syl2anc 411 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  ( P ( ball `  D
) +oo )  <->  ( x  e.  X  /\  ( P D x )  e.  RR ) ) )
5453simplbda 384 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) +oo ) )  -> 
( P D x )  e.  RR )
5547, 51, 54syl2anc 411 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( P D x )  e.  RR )
5646, 55readdcld 7964 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  (
( P D Q )  +  ( P D x ) )  e.  RR )
5756rexrd 7984 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  (
( P D Q )  +  ( P D x ) )  e.  RR* )
58 pnfxr 7987 . . . . . . . 8  |- +oo  e.  RR*
5958a1i 9 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  -> +oo  e.  RR* )
601ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  D  e.  (PsMet `  X )
)
612ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  P  e.  X )
628ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  Q  e.  X )
636adantr 276 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  x  e.  X )
6460, 61, 62, 63, 25syl13anc 1240 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( Q D x )  <_ 
( ( P D Q ) +e
( P D x ) ) )
6546, 55rexaddd 9828 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  (
( P D Q ) +e ( P D x ) )  =  ( ( P D Q )  +  ( P D x ) ) )
6664, 65breqtrd 4026 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( Q D x )  <_ 
( ( P D Q )  +  ( P D x ) ) )
67 ltpnf 9754 . . . . . . . 8  |-  ( ( ( P D Q )  +  ( P D x ) )  e.  RR  ->  (
( P D Q )  +  ( P D x ) )  < +oo )
6856, 67syl 14 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  (
( P D Q )  +  ( P D x ) )  < +oo )
6945, 57, 59, 66, 68xrlelttrd 9784 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( Q D x )  < +oo )
7019ad2antrr 488 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  S  e.  RR* )
71 xrpnfdc 9816 . . . . . . . 8  |-  ( S  e.  RR*  -> DECID  S  = +oo )
7270, 71syl 14 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  -> DECID  S  = +oo )
73 0xr 7981 . . . . . . . . . . 11  |-  0  e.  RR*
7473a1i 9 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  0  e.  RR* )
75 psmetge0 13464 . . . . . . . . . . 11  |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  Q  e.  X )  ->  0  <_  ( P D Q ) )
767, 21, 9, 75syl3anc 1238 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  0  <_  ( P D Q ) )
7774, 15, 35, 76, 37xrletrd 9786 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  0  <_  ( S +e  -e
R ) )
78 ge0nemnf 9798 . . . . . . . . 9  |-  ( ( ( S +e  -e R )  e. 
RR*  /\  0  <_  ( S +e  -e R ) )  ->  ( S +e  -e R )  =/= -oo )
7935, 77, 78syl2anc 411 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( S +e  -e R )  =/= -oo )
8079adantr 276 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( S +e  -e
R )  =/= -oo )
81 xaddmnf1 9822 . . . . . . . . . . . 12  |-  ( ( S  e.  RR*  /\  S  =/= +oo )  ->  ( S +e -oo )  = -oo )
8281ex 115 . . . . . . . . . . 11  |-  ( S  e.  RR*  ->  ( S  =/= +oo  ->  ( S +e -oo )  = -oo ) )
8370, 82syl 14 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( S  =/= +oo  ->  ( S +e -oo )  = -oo ) )
84 xnegeq 9801 . . . . . . . . . . . . . 14  |-  ( R  = +oo  ->  -e
R  =  -e +oo )
8549, 84syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  -e
R  =  -e +oo )
86 xnegpnf 9802 . . . . . . . . . . . . 13  |-  -e +oo  = -oo
8785, 86eqtrdi 2226 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  -e
R  = -oo )
8887oveq2d 5884 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( S +e  -e
R )  =  ( S +e -oo ) )
8988eqeq1d 2186 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  (
( S +e  -e R )  = -oo  <->  ( S +e -oo )  = -oo ) )
9083, 89sylibrd 169 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( S  =/= +oo  ->  ( S +e  -e
R )  = -oo ) )
9190a1d 22 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  (DECID  S  = +oo  ->  ( S  =/= +oo  ->  ( S +e  -e R )  = -oo )
) )
9291necon1ddc 2425 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  (DECID  S  = +oo  ->  ( ( S +e  -e
R )  =/= -oo  ->  S  = +oo )
) )
9372, 80, 92mp2d 47 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  S  = +oo )
9469, 93breqtrrd 4028 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( P ( ball `  D ) R ) )  /\  R  = +oo )  ->  ( Q D x )  < 
S )
95 psmetge0 13464 . . . . . . . . . . 11  |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  x  e.  X )  ->  0  <_  ( P D x ) )
967, 21, 6, 95syl3anc 1238 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  0  <_  ( P D x ) )
9774, 23, 16, 96, 27xrlelttrd 9784 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  0  <  R
)
9874, 16, 97xrltled 9773 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  0  <_  R
)
99 ge0nemnf 9798 . . . . . . . 8  |-  ( ( R  e.  RR*  /\  0  <_  R )  ->  R  =/= -oo )
10016, 98, 99syl2anc 411 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  R  =/= -oo )
10116, 100jca 306 . . . . . 6  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( R  e. 
RR*  /\  R  =/= -oo ) )
102 xrnemnf 9751 . . . . . 6  |-  ( ( R  e.  RR*  /\  R  =/= -oo )  <->  ( R  e.  RR  \/  R  = +oo ) )
103101, 102sylib 122 . . . . 5  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( R  e.  RR  \/  R  = +oo ) )
10444, 94, 103mpjaodan 798 . . . 4  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( Q D x )  <  S
)
105 elblps 13523 . . . . 5  |-  ( ( D  e.  (PsMet `  X )  /\  Q  e.  X  /\  S  e. 
RR* )  ->  (
x  e.  ( Q ( ball `  D
) S )  <->  ( x  e.  X  /\  ( Q D x )  < 
S ) ) )
1067, 9, 33, 105syl3anc 1238 . . . 4  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  ( x  e.  ( Q ( ball `  D ) S )  <-> 
( x  e.  X  /\  ( Q D x )  <  S ) ) )
1076, 104, 106mpbir2and 944 . . 3  |-  ( (
ph  /\  x  e.  ( P ( ball `  D
) R ) )  ->  x  e.  ( Q ( ball `  D
) S ) )
108107ex 115 . 2  |-  ( ph  ->  ( x  e.  ( P ( ball `  D
) R )  ->  x  e.  ( Q
( ball `  D ) S ) ) )
109108ssrdv 3161 1  |-  ( ph  ->  ( P ( ball `  D ) R ) 
C_  ( Q (
ball `  D ) S ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 708  DECID wdc 834    = wceq 1353    e. wcel 2148    =/= wne 2347    C_ wss 3129   class class class wbr 4000   ` cfv 5211  (class class class)co 5868   RRcr 7788   0cc0 7789    + caddc 7792   +oocpnf 7966   -oocmnf 7967   RR*cxr 7968    < clt 7969    <_ cle 7970    -ecxne 9743   +ecxad 9744  PsMetcpsmet 13112   ballcbl 13115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205  ax-un 4429  ax-setind 4532  ax-cnex 7880  ax-resscn 7881  ax-1cn 7882  ax-1re 7883  ax-icn 7884  ax-addcl 7885  ax-addrcl 7886  ax-mulcl 7887  ax-mulrcl 7888  ax-addcom 7889  ax-mulcom 7890  ax-addass 7891  ax-mulass 7892  ax-distr 7893  ax-i2m1 7894  ax-0lt1 7895  ax-1rid 7896  ax-0id 7897  ax-rnegex 7898  ax-precex 7899  ax-cnre 7900  ax-pre-ltirr 7901  ax-pre-ltwlin 7902  ax-pre-lttrn 7903  ax-pre-apti 7904  ax-pre-ltadd 7905  ax-pre-mulgt0 7906
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4289  df-po 4292  df-iso 4293  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-rn 4633  df-res 4634  df-ima 4635  df-iota 5173  df-fun 5213  df-fn 5214  df-f 5215  df-fv 5219  df-riota 5824  df-ov 5871  df-oprab 5872  df-mpo 5873  df-1st 6134  df-2nd 6135  df-map 6643  df-pnf 7971  df-mnf 7972  df-xr 7973  df-ltxr 7974  df-le 7975  df-sub 8107  df-neg 8108  df-2 8954  df-xneg 9746  df-xadd 9747  df-psmet 13120  df-bl 13123
This theorem is referenced by:  blss2ps  13539  ssblps  13558
  Copyright terms: Public domain W3C validator