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

Theorem boxcutc 6859
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 3298 . . 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 452 . 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 3199 . . . . . 6  |-  ( ( B  \  C )  =  if ( k  =  X ,  ( B  \  C ) ,  B )  -> 
( ( B  \  C )  C_  B  <->  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  B )
)
4 sseq1 3199 . . . . . 6  |-  ( B  =  if ( k  =  X ,  ( B  \  C ) ,  B )  -> 
( B  C_  B  <->  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  B )
)
5 difss 3303 . . . . . 6  |-  ( B 
\  C )  C_  B
6 ssid 3197 . . . . . 6  |-  B  C_  B
73, 4, 5, 6keephyp 3619 . . . . 5  |-  if ( k  =  X , 
( B  \  C
) ,  B ) 
C_  B
87rgenw 2610 . . . 4  |-  A. k  e.  A  if (
k  =  X , 
( B  \  C
) ,  B ) 
C_  B
9 ss2ixp 6829 . . . 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 11 . . 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 3180 . 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 6822 . . . . . . . . 9  |-  ( z  e.  X_ k  e.  A  B  ->  z  Fn  A
)
1312adantl 452 . . . . . . . 8  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  -> 
z  Fn  A )
1413biantrurd 494 . . . . . . 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 2791 . . . . . . . 8  |-  z  e. 
_V
1615elixp 6823 . . . . . . 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 255 . . . . . 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 285 . . . . 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 2554 . . . . . 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 2344 . . . . . . . . . 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 2344 . . . . . . . . . 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 2344 . . . . . . . . . . . . . . . . . . 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 2344 . . . . . . . . . . . . . . . . . . 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 443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  ->  X  e.  A )
2515elixp 6823 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  X_ k  e.  A  B 
<->  ( z  Fn  A  /\  A. k  e.  A  ( z `  k
)  e.  B ) )
2625simprbi 450 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  X_ k  e.  A  B  ->  A. k  e.  A  ( z `  k
)  e.  B )
27 nfv 1605 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ l ( z `  k
)  e.  B
28 nfcsb1v 3113 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ k [_ l  /  k ]_ B
2928nfel2 2431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ k ( z `  l
)  e.  [_ l  /  k ]_ B
30 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  l  ->  (
z `  k )  =  ( z `  l ) )
31 csbeq1a 3089 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  l  ->  B  =  [_ l  /  k ]_ B )
3230, 31eleq12d 2351 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  l  ->  (
( z `  k
)  e.  B  <->  ( z `  l )  e.  [_ l  /  k ]_ B
) )
3327, 29, 32cbvral 2760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. k  e.  A  (
z `  k )  e.  B  <->  A. l  e.  A  ( z `  l
)  e.  [_ l  /  k ]_ B
)
3426, 33sylib 188 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  X_ k  e.  A  B  ->  A. l  e.  A  ( z `  l
)  e.  [_ l  /  k ]_ B
)
35 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( l  =  X  ->  (
z `  l )  =  ( z `  X ) )
36 csbeq1 3084 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( l  =  X  ->  [_ l  /  k ]_ B  =  [_ X  /  k ]_ B )
3735, 36eleq12d 2351 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( l  =  X  ->  (
( z `  l
)  e.  [_ l  /  k ]_ B  <->  ( z `  X )  e.  [_ X  / 
k ]_ B ) )
3837rspcva 2882 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X  e.  A  /\  A. l  e.  A  ( z `  l )  e.  [_ l  / 
k ]_ B )  -> 
( z `  X
)  e.  [_ X  /  k ]_ B
)
3924, 34, 38syl2an 463 . . . . . . . . . . . . . . . . . . . . . . 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 3301 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( z `  X
)  e.  [_ X  /  k ]_ B  /\  -.  ( z `  X )  e.  (
[_ X  /  k ]_ B  \  [_ X  /  k ]_ C
) )  ->  (
z `  X )  e.  [_ X  /  k ]_ C )
4139, 40sylan 457 . . . . . . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . . . 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 3084 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  X  ->  [_ l  /  k ]_ C  =  [_ X  /  k ]_ C )
4435, 43eleq12d 2351 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  X  ->  (
( z `  l
)  e.  [_ l  /  k ]_ C  <->  ( z `  X )  e.  [_ X  / 
k ]_ C ) )
4542, 44syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . 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 418 . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . 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 2641 . . . . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . 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 3595 . . . . . . . . . . . . . . . . . 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 2626 . . . . . . . . . . . . . . . . 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 2555 . . . . . . . . . . . . . . . . 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 188 . . . . . . . . . . . . . . . 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 423 . . . . . . . . . . . . . . 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 97 . . . . . . . . . . . . . 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 418 . . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 5525 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  (
z `  m )  =  ( z `  X ) )
59 csbeq1 3084 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  [_ m  /  k ]_ B  =  [_ X  /  k ]_ B )
60 csbeq1 3084 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  [_ m  /  k ]_ C  =  [_ X  /  k ]_ C )
6159, 60difeq12d 3295 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  ( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
)  =  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )
6258, 61eleq12d 2351 . . . . . . . . . . . 12  |-  ( m  =  X  ->  (
( z `  m
)  e.  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C )  <->  ( z `  X )  e.  (
[_ X  /  k ]_ B  \  [_ X  /  k ]_ C
) ) )
6357, 62syl5ibrcom 213 . . . . . . . . . . 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 418 . . . . . . . . . 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 1605 . . . . . . . . . . . . . . 15  |-  F/ m
( z `  k
)  e.  B
66 nfcsb1v 3113 . . . . . . . . . . . . . . . 16  |-  F/_ k [_ m  /  k ]_ B
6766nfel2 2431 . . . . . . . . . . . . . . 15  |-  F/ k ( z `  m
)  e.  [_ m  /  k ]_ B
68 fveq2 5525 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  (
z `  k )  =  ( z `  m ) )
69 csbeq1a 3089 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  B  =  [_ m  /  k ]_ B )
7068, 69eleq12d 2351 . . . . . . . . . . . . . . 15  |-  ( k  =  m  ->  (
( z `  k
)  e.  B  <->  ( z `  m )  e.  [_ m  /  k ]_ B
) )
7165, 67, 70cbvral 2760 . . . . . . . . . . . . . 14  |-  ( A. k  e.  A  (
z `  k )  e.  B  <->  A. m  e.  A  ( z `  m
)  e.  [_ m  /  k ]_ B
)
7226, 71sylib 188 . . . . . . . . . . . . 13  |-  ( z  e.  X_ k  e.  A  B  ->  A. m  e.  A  ( z `  m
)  e.  [_ m  /  k ]_ B
)
7372ad2antlr 707 . . . . . . . . . . . 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 2641 . . . . . . . . . . 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 451 . . . . . . . . . 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 3595 . . . . . . . . 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 2626 . . . . . . . 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 734 . . . . . . . . 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 730 . . . . . . . . . . 11  |-  ( ( ( X  e.  A  /\  A. k  e.  A  C  C_  B )  /\  z  e.  X_ k  e.  A  B )  ->  X  e.  A )
80 iftrue 3571 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)  =  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) )
8180, 61eqtrd 2315 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)  =  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )
8258, 81eleq12d 2351 . . . . . . . . . . . 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 2882 . . . . . . . . . . 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 457 . . . . . . . . . 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
) )
85 eldifn 3299 . . . . . . . . . 10  |-  ( ( z `  X )  e.  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C )  ->  -.  ( z `  X
)  e.  [_ X  /  k ]_ C
)
8684, 85syl 15 . . . . . . . . 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
)
87 iftrue 3571 . . . . . . . . . . . . 13  |-  ( l  =  X  ->  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)  =  [_ l  /  k ]_ C
)
8887, 43eqtrd 2315 . . . . . . . . . . . 12  |-  ( l  =  X  ->  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)  =  [_ X  /  k ]_ C
)
8935, 88eleq12d 2351 . . . . . . . . . . 11  |-  ( l  =  X  ->  (
( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
)  <->  ( z `  X )  e.  [_ X  /  k ]_ C
) )
9089notbid 285 . . . . . . . . . 10  |-  ( l  =  X  ->  ( -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
)  <->  -.  ( z `  X )  e.  [_ X  /  k ]_ C
) )
9190rspcev 2884 . . . . . . . . 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 ) )
9278, 86, 91syl2anc 642 . . . . . . . 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 ) )
9377, 92impbida 805 . . . . . . 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
) ) )
94 nfv 1605 . . . . . . . 8  |-  F/ l  -.  ( z `  k )  e.  if ( k  =  X ,  C ,  B
)
95 nfv 1605 . . . . . . . . . . 11  |-  F/ k  l  =  X
96 nfcsb1v 3113 . . . . . . . . . . 11  |-  F/_ k [_ l  /  k ]_ C
9795, 96, 28nfif 3589 . . . . . . . . . 10  |-  F/_ k if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)
9897nfel2 2431 . . . . . . . . 9  |-  F/ k ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
)
9998nfn 1765 . . . . . . . 8  |-  F/ k  -.  ( z `  l )  e.  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)
100 eqeq1 2289 . . . . . . . . . . 11  |-  ( k  =  l  ->  (
k  =  X  <->  l  =  X ) )
101 csbeq1a 3089 . . . . . . . . . . 11  |-  ( k  =  l  ->  C  =  [_ l  /  k ]_ C )
102100, 101, 31ifbieq12d 3587 . . . . . . . . . 10  |-  ( k  =  l  ->  if ( k  =  X ,  C ,  B
)  =  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )
10330, 102eleq12d 2351 . . . . . . . . 9  |-  ( k  =  l  ->  (
( z `  k
)  e.  if ( k  =  X ,  C ,  B )  <->  ( z `  l )  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B ) ) )
104103notbid 285 . . . . . . . 8  |-  ( k  =  l  ->  ( -.  ( z `  k
)  e.  if ( k  =  X ,  C ,  B )  <->  -.  ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) ) )
10594, 99, 104cbvrex 2761 . . . . . . 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
) )
106 nfv 1605 . . . . . . . 8  |-  F/ m
( z `  k
)  e.  if ( k  =  X , 
( B  \  C
) ,  B )
107 nfv 1605 . . . . . . . . . 10  |-  F/ k  m  =  X
108 nfcsb1v 3113 . . . . . . . . . . 11  |-  F/_ k [_ m  /  k ]_ C
10966, 108nfdif 3297 . . . . . . . . . 10  |-  F/_ k
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
)
110107, 109, 66nfif 3589 . . . . . . . . 9  |-  F/_ k if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)
111110nfel2 2431 . . . . . . . 8  |-  F/ k ( z `  m
)  e.  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
)
112 eqeq1 2289 . . . . . . . . . 10  |-  ( k  =  m  ->  (
k  =  X  <->  m  =  X ) )
113 csbeq1a 3089 . . . . . . . . . . 11  |-  ( k  =  m  ->  C  =  [_ m  /  k ]_ C )
11469, 113difeq12d 3295 . . . . . . . . . 10  |-  ( k  =  m  ->  ( B  \  C )  =  ( [_ m  / 
k ]_ B  \  [_ m  /  k ]_ C
) )
115112, 114, 69ifbieq12d 3587 . . . . . . . . 9  |-  ( k  =  m  ->  if ( k  =  X ,  ( B  \  C ) ,  B
)  =  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
) )
11668, 115eleq12d 2351 . . . . . . . 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
) ) )
117106, 111, 116cbvral 2760 . . . . . . 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
) )
11893, 105, 1173bitr4g 279 . . . . . 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
) ) )
11919, 118syl5bbr 250 . . . . 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 ) ) )
12018, 119bitrd 244 . . . 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 ) ) )
121 ibar 490 . . . . 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
) ) ) )
122121adantl 452 . . . 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
) ) ) )
12313biantrurd 494 . . . 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
) ) ) )
124120, 122, 1233bitr3d 274 . . 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
) ) ) )
125 eldif 3162 . . 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
) ) )
12615elixp 6823 . . 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
) ) )
127124, 125, 1263bitr4g 279 . 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
) ) )
1282, 11, 127eqrdav 2282 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 176    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543   E.wrex 2544   [_csb 3081    \ cdif 3149    C_ wss 3152   ifcif 3565    Fn wfn 5250   ` cfv 5255   X_cixp 6817
This theorem is referenced by:  ptcld  17307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fn 5258  df-fv 5263  df-ixp 6818
  Copyright terms: Public domain W3C validator