MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  boxcutc Structured version   Unicode version

Theorem boxcutc 7106
Description: The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Assertion
Ref Expression
boxcutc  |-  ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  ->  ( X_ k  e.  A  B  \ 
X_ k  e.  A  if ( k  =  X ,  C ,  B
) )  =  X_ k  e.  A  if ( k  =  X ,  ( B  \  C ) ,  B
) )
Distinct variable groups:    A, k    k, X
Allowed substitution hints:    B( k)    C( k)

Proof of Theorem boxcutc
Dummy variables  l  m  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 3470 . . 3  |-  ( z  e.  ( X_ k  e.  A  B  \  X_ k  e.  A  if (
k  =  X ,  C ,  B )
)  ->  z  e.  X_ k  e.  A  B
)
21adantl 454 . 2  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  ( X_ k  e.  A  B  \ 
X_ k  e.  A  if ( k  =  X ,  C ,  B
) ) )  -> 
z  e.  X_ k  e.  A  B )
3 sseq1 3370 . . . . . 6  |-  ( ( B  \  C )  =  if ( k  =  X ,  ( B  \  C ) ,  B )  -> 
( ( B  \  C )  C_  B  <->  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  B )
)
4 sseq1 3370 . . . . . 6  |-  ( B  =  if ( k  =  X ,  ( B  \  C ) ,  B )  -> 
( B  C_  B  <->  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  B )
)
5 difss 3475 . . . . . 6  |-  ( B 
\  C )  C_  B
6 ssid 3368 . . . . . 6  |-  B  C_  B
73, 4, 5, 6keephyp 3794 . . . . 5  |-  if ( k  =  X , 
( B  \  C
) ,  B ) 
C_  B
87rgenw 2774 . . . 4  |-  A. k  e.  A  if (
k  =  X , 
( B  \  C
) ,  B ) 
C_  B
9 ss2ixp 7076 . . . 4  |-  ( A. k  e.  A  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  B  ->  X_ k  e.  A  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  X_ k  e.  A  B )
108, 9mp1i 12 . . 3  |-  ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  ->  X_ k  e.  A  if (
k  =  X , 
( B  \  C
) ,  B ) 
C_  X_ k  e.  A  B )
1110sselda 3349 . 2  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  if ( k  =  X ,  ( B  \  C ) ,  B ) )  ->  z  e.  X_ k  e.  A  B
)
12 ixpfn 7069 . . . . . . . . 9  |-  ( z  e.  X_ k  e.  A  B  ->  z  Fn  A
)
1312adantl 454 . . . . . . . 8  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
z  Fn  A )
1413biantrurd 496 . . . . . . 7  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  C ,  B
)  <->  ( z  Fn  A  /\  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  C ,  B
) ) ) )
15 vex 2960 . . . . . . . 8  |-  z  e. 
_V
1615elixp 7070 . . . . . . 7  |-  ( z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
)  <->  ( z  Fn  A  /\  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  C ,  B
) ) )
1714, 16syl6rbbr 257 . . . . . 6  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
)  <->  A. k  e.  A  ( z `  k
)  e.  if ( k  =  X ,  C ,  B )
) )
1817notbid 287 . . . . 5  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
)  <->  -.  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  C ,  B
) ) )
19 rexnal 2717 . . . . . 6  |-  ( E. k  e.  A  -.  ( z `  k
)  e.  if ( k  =  X ,  C ,  B )  <->  -. 
A. k  e.  A  ( z `  k
)  e.  if ( k  =  X ,  C ,  B )
)
20 eleq2 2498 . . . . . . . . . 10  |-  ( (
[_ m  /  k ]_ B  \  [_ m  /  k ]_ C
)  =  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
)  ->  ( (
z `  m )  e.  ( [_ m  / 
k ]_ B  \  [_ m  /  k ]_ C
)  <->  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) ) )
21 eleq2 2498 . . . . . . . . . 10  |-  ( [_ m  /  k ]_ B  =  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)  ->  ( (
z `  m )  e.  [_ m  /  k ]_ B  <->  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) ) )
22 eleq2 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( [_ l  /  k ]_ C  =  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B )  ->  (
( z `  l
)  e.  [_ l  /  k ]_ C  <->  ( z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) ) )
23 eleq2 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( [_ l  /  k ]_ B  =  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B )  ->  (
( z `  l
)  e.  [_ l  /  k ]_ B  <->  ( z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) ) )
24 simpl 445 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  ->  X  e.  A )
2515elixp 7070 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  X_ k  e.  A  B 
<->  ( z  Fn  A  /\  A. k  e.  A  ( z `  k
)  e.  B ) )
2625simprbi 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  X_ k  e.  A  B  ->  A. k  e.  A  ( z `  k
)  e.  B )
27 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ l ( z `  k
)  e.  B
28 nfcsb1v 3284 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ k [_ l  /  k ]_ B
2928nfel2 2585 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ k ( z `  l
)  e.  [_ l  /  k ]_ B
30 fveq2 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  l  ->  (
z `  k )  =  ( z `  l ) )
31 csbeq1a 3260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  l  ->  B  =  [_ l  /  k ]_ B )
3230, 31eleq12d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  l  ->  (
( z `  k
)  e.  B  <->  ( z `  l )  e.  [_ l  /  k ]_ B
) )
3327, 29, 32cbvral 2929 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. k  e.  A  (
z `  k )  e.  B  <->  A. l  e.  A  ( z `  l
)  e.  [_ l  /  k ]_ B
)
3426, 33sylib 190 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  X_ k  e.  A  B  ->  A. l  e.  A  ( z `  l
)  e.  [_ l  /  k ]_ B
)
35 fveq2 5729 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( l  =  X  ->  (
z `  l )  =  ( z `  X ) )
36 csbeq1 3255 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( l  =  X  ->  [_ l  /  k ]_ B  =  [_ X  /  k ]_ B )
3735, 36eleq12d 2505 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( l  =  X  ->  (
( z `  l
)  e.  [_ l  /  k ]_ B  <->  ( z `  X )  e.  [_ X  / 
k ]_ B ) )
3837rspcva 3051 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X  e.  A  /\  A. l  e.  A  ( z `  l )  e.  [_ l  / 
k ]_ B )  -> 
( z `  X
)  e.  [_ X  /  k ]_ B
)
3924, 34, 38syl2an 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( z `  X
)  e.  [_ X  /  k ]_ B
)
40 neldif 3473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( z `  X
)  e.  [_ X  /  k ]_ B  /\  -.  ( z `  X )  e.  (
[_ X  /  k ]_ B  \  [_ X  /  k ]_ C
) )  ->  (
z `  X )  e.  [_ X  /  k ]_ C )
4139, 40sylan 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  -.  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) )  ->  (
z `  X )  e.  [_ X  /  k ]_ C )
4241adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  -.  ( z `  X
)  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )  /\  l  e.  A )  ->  ( z `  X
)  e.  [_ X  /  k ]_ C
)
43 csbeq1 3255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  X  ->  [_ l  /  k ]_ C  =  [_ X  /  k ]_ C )
4435, 43eleq12d 2505 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  X  ->  (
( z `  l
)  e.  [_ l  /  k ]_ C  <->  ( z `  X )  e.  [_ X  / 
k ]_ C ) )
4542, 44syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  -.  ( z `  X
)  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )  /\  l  e.  A )  ->  ( l  =  X  ->  ( z `  l )  e.  [_ l  /  k ]_ C
) )
4645imp 420 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  -.  ( z `  X
)  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )  /\  l  e.  A )  /\  l  =  X
)  ->  ( z `  l )  e.  [_ l  /  k ]_ C
)
4734ad2antlr 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  -.  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) )  ->  A. l  e.  A  ( z `  l )  e.  [_ l  /  k ]_ B
)
4847r19.21bi 2805 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  -.  ( z `  X
)  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )  /\  l  e.  A )  ->  ( z `  l
)  e.  [_ l  /  k ]_ B
)
4948adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  -.  ( z `  X
)  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )  /\  l  e.  A )  /\  -.  l  =  X )  ->  ( z `  l )  e.  [_ l  /  k ]_ B
)
5022, 23, 46, 49ifbothda 3770 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  -.  ( z `  X
)  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )  /\  l  e.  A )  ->  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )
5150ralrimiva 2790 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  -.  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) )  ->  A. l  e.  A  ( z `  l )  e.  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
) )
52 dfral2 2718 . . . . . . . . . . . . . . . . 17  |-  ( A. l  e.  A  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B )  <->  -.  E. l  e.  A  -.  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) )
5351, 52sylib 190 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  -.  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) )  ->  -.  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )
5453ex 425 . . . . . . . . . . . . . . 15  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( -.  ( z `
 X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
)  ->  -.  E. l  e.  A  -.  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) ) )
5554con4d 100 . . . . . . . . . . . . . 14  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( E. l  e.  A  -.  ( z `
 l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B )  ->  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) ) )
5655imp 420 . . . . . . . . . . . . 13  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  E. l  e.  A  -.  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) )  -> 
( z `  X
)  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )
5756adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )  /\  m  e.  A )  ->  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) )
58 fveq2 5729 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  (
z `  m )  =  ( z `  X ) )
59 csbeq1 3255 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  [_ m  /  k ]_ B  =  [_ X  /  k ]_ B )
60 csbeq1 3255 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  [_ m  /  k ]_ C  =  [_ X  /  k ]_ C )
6159, 60difeq12d 3467 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  ( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
)  =  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )
6258, 61eleq12d 2505 . . . . . . . . . . . 12  |-  ( m  =  X  ->  (
( z `  m
)  e.  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C )  <->  ( z `  X )  e.  (
[_ X  /  k ]_ B  \  [_ X  /  k ]_ C
) ) )
6357, 62syl5ibrcom 215 . . . . . . . . . . 11  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )  /\  m  e.  A )  ->  (
m  =  X  -> 
( z `  m
)  e.  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ) )
6463imp 420 . . . . . . . . . 10  |-  ( ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )  /\  m  e.  A )  /\  m  =  X )  ->  (
z `  m )  e.  ( [_ m  / 
k ]_ B  \  [_ m  /  k ]_ C
) )
65 nfv 1630 . . . . . . . . . . . . . . 15  |-  F/ m
( z `  k
)  e.  B
66 nfcsb1v 3284 . . . . . . . . . . . . . . . 16  |-  F/_ k [_ m  /  k ]_ B
6766nfel2 2585 . . . . . . . . . . . . . . 15  |-  F/ k ( z `  m
)  e.  [_ m  /  k ]_ B
68 fveq2 5729 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  (
z `  k )  =  ( z `  m ) )
69 csbeq1a 3260 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  B  =  [_ m  /  k ]_ B )
7068, 69eleq12d 2505 . . . . . . . . . . . . . . 15  |-  ( k  =  m  ->  (
( z `  k
)  e.  B  <->  ( z `  m )  e.  [_ m  /  k ]_ B
) )
7165, 67, 70cbvral 2929 . . . . . . . . . . . . . 14  |-  ( A. k  e.  A  (
z `  k )  e.  B  <->  A. m  e.  A  ( z `  m
)  e.  [_ m  /  k ]_ B
)
7226, 71sylib 190 . . . . . . . . . . . . 13  |-  ( z  e.  X_ k  e.  A  B  ->  A. m  e.  A  ( z `  m
)  e.  [_ m  /  k ]_ B
)
7372ad2antlr 709 . . . . . . . . . . . 12  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  E. l  e.  A  -.  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) )  ->  A. m  e.  A  ( z `  m
)  e.  [_ m  /  k ]_ B
)
7473r19.21bi 2805 . . . . . . . . . . 11  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )  /\  m  e.  A )  ->  (
z `  m )  e.  [_ m  /  k ]_ B )
7574adantr 453 . . . . . . . . . 10  |-  ( ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )  /\  m  e.  A )  /\  -.  m  =  X )  ->  ( z `  m
)  e.  [_ m  /  k ]_ B
)
7620, 21, 64, 75ifbothda 3770 . . . . . . . . 9  |-  ( ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  /\  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )  /\  m  e.  A )  ->  (
z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) )
7776ralrimiva 2790 . . . . . . . 8  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  E. l  e.  A  -.  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) )  ->  A. m  e.  A  ( z `  m
)  e.  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
) )
78 simplll 736 . . . . . . . . 9  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  A. m  e.  A  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) )  ->  X  e.  A )
79 simpll 732 . . . . . . . . . . 11  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  ->  X  e.  A )
80 iftrue 3746 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)  =  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) )
8180, 61eqtrd 2469 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)  =  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )
8258, 81eleq12d 2505 . . . . . . . . . . . 12  |-  ( m  =  X  ->  (
( z `  m
)  e.  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
)  <->  ( z `  X )  e.  (
[_ X  /  k ]_ B  \  [_ X  /  k ]_ C
) ) )
8382rspcva 3051 . . . . . . . . . . 11  |-  ( ( X  e.  A  /\  A. m  e.  A  ( z `  m )  e.  if ( m  =  X ,  (
[_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
) )  ->  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) )
8479, 83sylan 459 . . . . . . . . . 10  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  A. m  e.  A  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) )  ->  (
z `  X )  e.  ( [_ X  / 
k ]_ B  \  [_ X  /  k ]_ C
) )
8584eldifbd 3334 . . . . . . . . 9  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  A. m  e.  A  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) )  ->  -.  ( z `  X
)  e.  [_ X  /  k ]_ C
)
86 iftrue 3746 . . . . . . . . . . . . 13  |-  ( l  =  X  ->  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)  =  [_ l  /  k ]_ C
)
8786, 43eqtrd 2469 . . . . . . . . . . . 12  |-  ( l  =  X  ->  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)  =  [_ X  /  k ]_ C
)
8835, 87eleq12d 2505 . . . . . . . . . . 11  |-  ( l  =  X  ->  (
( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
)  <->  ( z `  X )  e.  [_ X  /  k ]_ C
) )
8988notbid 287 . . . . . . . . . 10  |-  ( l  =  X  ->  ( -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
)  <->  -.  ( z `  X )  e.  [_ X  /  k ]_ C
) )
9089rspcev 3053 . . . . . . . . 9  |-  ( ( X  e.  A  /\  -.  ( z `  X
)  e.  [_ X  /  k ]_ C
)  ->  E. l  e.  A  -.  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) )
9178, 85, 90syl2anc 644 . . . . . . . 8  |-  ( ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B
)  /\  z  e.  X_ k  e.  A  B
)  /\  A. m  e.  A  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) )  ->  E. l  e.  A  -.  (
z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) )
9277, 91impbida 807 . . . . . . 7  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( E. l  e.  A  -.  ( z `
 l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B )  <->  A. m  e.  A  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) ) )
93 nfv 1630 . . . . . . . 8  |-  F/ l  -.  ( z `  k )  e.  if ( k  =  X ,  C ,  B
)
94 nfv 1630 . . . . . . . . . . 11  |-  F/ k  l  =  X
95 nfcsb1v 3284 . . . . . . . . . . 11  |-  F/_ k [_ l  /  k ]_ C
9694, 95, 28nfif 3764 . . . . . . . . . 10  |-  F/_ k if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)
9796nfel2 2585 . . . . . . . . 9  |-  F/ k ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
)
9897nfn 1812 . . . . . . . 8  |-  F/ k  -.  ( z `  l )  e.  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)
99 eqeq1 2443 . . . . . . . . . . 11  |-  ( k  =  l  ->  (
k  =  X  <->  l  =  X ) )
100 csbeq1a 3260 . . . . . . . . . . 11  |-  ( k  =  l  ->  C  =  [_ l  /  k ]_ C )
10199, 100, 31ifbieq12d 3762 . . . . . . . . . 10  |-  ( k  =  l  ->  if ( k  =  X ,  C ,  B
)  =  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )
10230, 101eleq12d 2505 . . . . . . . . 9  |-  ( k  =  l  ->  (
( z `  k
)  e.  if ( k  =  X ,  C ,  B )  <->  ( z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) ) )
103102notbid 287 . . . . . . . 8  |-  ( k  =  l  ->  ( -.  ( z `  k
)  e.  if ( k  =  X ,  C ,  B )  <->  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) ) )
10493, 98, 103cbvrex 2930 . . . . . . 7  |-  ( E. k  e.  A  -.  ( z `  k
)  e.  if ( k  =  X ,  C ,  B )  <->  E. l  e.  A  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )
105 nfv 1630 . . . . . . . 8  |-  F/ m
( z `  k
)  e.  if ( k  =  X , 
( B  \  C
) ,  B )
106 nfv 1630 . . . . . . . . . 10  |-  F/ k  m  =  X
107 nfcsb1v 3284 . . . . . . . . . . 11  |-  F/_ k [_ m  /  k ]_ C
10866, 107nfdif 3469 . . . . . . . . . 10  |-  F/_ k
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
)
109106, 108, 66nfif 3764 . . . . . . . . 9  |-  F/_ k if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)
110109nfel2 2585 . . . . . . . 8  |-  F/ k ( z `  m
)  e.  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
)
111 eqeq1 2443 . . . . . . . . . 10  |-  ( k  =  m  ->  (
k  =  X  <->  m  =  X ) )
112 csbeq1a 3260 . . . . . . . . . . 11  |-  ( k  =  m  ->  C  =  [_ m  /  k ]_ C )
11369, 112difeq12d 3467 . . . . . . . . . 10  |-  ( k  =  m  ->  ( B  \  C )  =  ( [_ m  / 
k ]_ B  \  [_ m  /  k ]_ C
) )
114111, 113, 69ifbieq12d 3762 . . . . . . . . 9  |-  ( k  =  m  ->  if ( k  =  X ,  ( B  \  C ) ,  B
)  =  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
) )
11568, 114eleq12d 2505 . . . . . . . 8  |-  ( k  =  m  ->  (
( z `  k
)  e.  if ( k  =  X , 
( B  \  C
) ,  B )  <-> 
( z `  m
)  e.  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
) ) )
116105, 110, 115cbvral 2929 . . . . . . 7  |-  ( A. k  e.  A  (
z `  k )  e.  if ( k  =  X ,  ( B 
\  C ) ,  B )  <->  A. m  e.  A  ( z `  m )  e.  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
) )
11792, 104, 1163bitr4g 281 . . . . . 6  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( E. k  e.  A  -.  ( z `
 k )  e.  if ( k  =  X ,  C ,  B )  <->  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  ( B  \  C ) ,  B
) ) )
11819, 117syl5bbr 252 . . . . 5  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( -.  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  C ,  B
)  <->  A. k  e.  A  ( z `  k
)  e.  if ( k  =  X , 
( B  \  C
) ,  B ) ) )
11918, 118bitrd 246 . . . 4  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
)  <->  A. k  e.  A  ( z `  k
)  e.  if ( k  =  X , 
( B  \  C
) ,  B ) ) )
120 ibar 492 . . . . 5  |-  ( z  e.  X_ k  e.  A  B  ->  ( -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
)  <->  ( z  e.  X_ k  e.  A  B  /\  -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
) ) ) )
121120adantl 454 . . . 4  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
)  <->  ( z  e.  X_ k  e.  A  B  /\  -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
) ) ) )
12213biantrurd 496 . . . 4  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  ( B  \  C ) ,  B
)  <->  ( z  Fn  A  /\  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  ( B  \  C ) ,  B
) ) ) )
123119, 121, 1223bitr3d 276 . . 3  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( ( z  e.  X_ k  e.  A  B  /\  -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
) )  <->  ( z  Fn  A  /\  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  ( B  \  C ) ,  B
) ) ) )
124 eldif 3331 . . 3  |-  ( z  e.  ( X_ k  e.  A  B  \  X_ k  e.  A  if (
k  =  X ,  C ,  B )
)  <->  ( z  e.  X_ k  e.  A  B  /\  -.  z  e.  X_ k  e.  A  if ( k  =  X ,  C ,  B
) ) )
12515elixp 7070 . . 3  |-  ( z  e.  X_ k  e.  A  if ( k  =  X ,  ( B  \  C ) ,  B
)  <->  ( z  Fn  A  /\  A. k  e.  A  ( z `  k )  e.  if ( k  =  X ,  ( B  \  C ) ,  B
) ) )
126123, 124, 1253bitr4g 281 . 2  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
( z  e.  (
X_ k  e.  A  B  \  X_ k  e.  A  if ( k  =  X ,  C ,  B
) )  <->  z  e.  X_ k  e.  A  if ( k  =  X ,  ( B  \  C ) ,  B
) ) )
1272, 11, 126eqrdav 2436 1  |-  ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  ->  ( X_ k  e.  A  B  \ 
X_ k  e.  A  if ( k  =  X ,  C ,  B
) )  =  X_ k  e.  A  if ( k  =  X ,  ( B  \  C ) ,  B
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2706   E.wrex 2707   [_csb 3252    \ cdif 3318    C_ wss 3321   ifcif 3740    Fn wfn 5450   ` cfv 5455   X_cixp 7064
This theorem is referenced by:  ptcld  17646
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-opab 4268  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-iota 5419  df-fun 5457  df-fn 5458  df-fv 5463  df-ixp 7065
  Copyright terms: Public domain W3C validator