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

Theorem boxcutc 6875
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 3311 . . 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 3212 . . . . . 6  |-  ( ( B  \  C )  =  if ( k  =  X ,  ( B  \  C ) ,  B )  -> 
( ( B  \  C )  C_  B  <->  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  B )
)
4 sseq1 3212 . . . . . 6  |-  ( B  =  if ( k  =  X ,  ( B  \  C ) ,  B )  -> 
( B  C_  B  <->  if ( k  =  X ,  ( B  \  C ) ,  B
)  C_  B )
)
5 difss 3316 . . . . . 6  |-  ( B 
\  C )  C_  B
6 ssid 3210 . . . . . 6  |-  B  C_  B
73, 4, 5, 6keephyp 3632 . . . . 5  |-  if ( k  =  X , 
( B  \  C
) ,  B ) 
C_  B
87rgenw 2623 . . . 4  |-  A. k  e.  A  if (
k  =  X , 
( B  \  C
) ,  B ) 
C_  B
9 ss2ixp 6845 . . . 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 3193 . 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 6838 . . . . . . . . 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 2804 . . . . . . . 8  |-  z  e. 
_V
1615elixp 6839 . . . . . . 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 2567 . . . . . 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 2357 . . . . . . . . . 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 2357 . . . . . . . . . 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 2357 . . . . . . . . . . . . . . . . . . 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 2357 . . . . . . . . . . . . . . . . . . 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 6839 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1609 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ l ( z `  k
)  e.  B
28 nfcsb1v 3126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ k [_ l  /  k ]_ B
2928nfel2 2444 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ k ( z `  l
)  e.  [_ l  /  k ]_ B
30 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  l  ->  (
z `  k )  =  ( z `  l ) )
31 csbeq1a 3102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  l  ->  B  =  [_ l  /  k ]_ B )
3230, 31eleq12d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  l  ->  (
( z `  k
)  e.  B  <->  ( z `  l )  e.  [_ l  /  k ]_ B
) )
3327, 29, 32cbvral 2773 . . . . . . . . . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( l  =  X  ->  (
z `  l )  =  ( z `  X ) )
36 csbeq1 3097 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( l  =  X  ->  [_ l  /  k ]_ B  =  [_ X  /  k ]_ B )
3735, 36eleq12d 2364 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( l  =  X  ->  (
( z `  l
)  e.  [_ l  /  k ]_ B  <->  ( z `  X )  e.  [_ X  / 
k ]_ B ) )
3837rspcva 2895 . . . . . . . . . . . . . . . . . . . . . . . 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 3314 . . . . . . . . . . . . . . . . . . . . . . 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 3097 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  X  ->  [_ l  /  k ]_ C  =  [_ X  /  k ]_ C )
4435, 43eleq12d 2364 . . . . . . . . . . . . . . . . . . . . 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 2654 . . . . . . . . . . . . . . . . . . . 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 3608 . . . . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . . . . . 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 2568 . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  (
z `  m )  =  ( z `  X ) )
59 csbeq1 3097 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  [_ m  /  k ]_ B  =  [_ X  /  k ]_ B )
60 csbeq1 3097 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  [_ m  /  k ]_ C  =  [_ X  /  k ]_ C )
6159, 60difeq12d 3308 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  ( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
)  =  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )
6258, 61eleq12d 2364 . . . . . . . . . . . 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 1609 . . . . . . . . . . . . . . 15  |-  F/ m
( z `  k
)  e.  B
66 nfcsb1v 3126 . . . . . . . . . . . . . . . 16  |-  F/_ k [_ m  /  k ]_ B
6766nfel2 2444 . . . . . . . . . . . . . . 15  |-  F/ k ( z `  m
)  e.  [_ m  /  k ]_ B
68 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  (
z `  k )  =  ( z `  m ) )
69 csbeq1a 3102 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  B  =  [_ m  /  k ]_ B )
7068, 69eleq12d 2364 . . . . . . . . . . . . . . 15  |-  ( k  =  m  ->  (
( z `  k
)  e.  B  <->  ( z `  m )  e.  [_ m  /  k ]_ B
) )
7165, 67, 70cbvral 2773 . . . . . . . . . . . . . 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 2654 . . . . . . . . . . 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 3608 . . . . . . . . 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 2639 . . . . . . . 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 3584 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)  =  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) )
8180, 61eqtrd 2328 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)  =  ( [_ X  /  k ]_ B  \ 
[_ X  /  k ]_ C ) )
8258, 81eleq12d 2364 . . . . . . . . . . . 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 2895 . . . . . . . . . . 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 3312 . . . . . . . . . 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 3584 . . . . . . . . . . . . 13  |-  ( l  =  X  ->  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)  =  [_ l  /  k ]_ C
)
8887, 43eqtrd 2328 . . . . . . . . . . . 12  |-  ( l  =  X  ->  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)  =  [_ X  /  k ]_ C
)
8935, 88eleq12d 2364 . . . . . . . . . . 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 2897 . . . . . . . . 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 1609 . . . . . . . 8  |-  F/ l  -.  ( z `  k )  e.  if ( k  =  X ,  C ,  B
)
95 nfv 1609 . . . . . . . . . . 11  |-  F/ k  l  =  X
96 nfcsb1v 3126 . . . . . . . . . . 11  |-  F/_ k [_ l  /  k ]_ C
9795, 96, 28nfif 3602 . . . . . . . . . 10  |-  F/_ k if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)
9897nfel2 2444 . . . . . . . . 9  |-  F/ k ( z `  l
)  e.  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
)
9998nfn 1777 . . . . . . . 8  |-  F/ k  -.  ( z `  l )  e.  if ( l  =  X ,  [_ l  / 
k ]_ C ,  [_ l  /  k ]_ B
)
100 eqeq1 2302 . . . . . . . . . . 11  |-  ( k  =  l  ->  (
k  =  X  <->  l  =  X ) )
101 csbeq1a 3102 . . . . . . . . . . 11  |-  ( k  =  l  ->  C  =  [_ l  /  k ]_ C )
102100, 101, 31ifbieq12d 3600 . . . . . . . . . 10  |-  ( k  =  l  ->  if ( k  =  X ,  C ,  B
)  =  if ( l  =  X ,  [_ l  /  k ]_ C ,  [_ l  /  k ]_ B
) )
10330, 102eleq12d 2364 . . . . . . . . 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 2774 . . . . . . 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 1609 . . . . . . . 8  |-  F/ m
( z `  k
)  e.  if ( k  =  X , 
( B  \  C
) ,  B )
107 nfv 1609 . . . . . . . . . 10  |-  F/ k  m  =  X
108 nfcsb1v 3126 . . . . . . . . . . 11  |-  F/_ k [_ m  /  k ]_ C
10966, 108nfdif 3310 . . . . . . . . . 10  |-  F/_ k
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
)
110107, 109, 66nfif 3602 . . . . . . . . 9  |-  F/_ k if ( m  =  X ,  ( [_ m  /  k ]_ B  \ 
[_ m  /  k ]_ C ) ,  [_ m  /  k ]_ B
)
111110nfel2 2444 . . . . . . . 8  |-  F/ k ( z `  m
)  e.  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
)
112 eqeq1 2302 . . . . . . . . . 10  |-  ( k  =  m  ->  (
k  =  X  <->  m  =  X ) )
113 csbeq1a 3102 . . . . . . . . . . 11  |-  ( k  =  m  ->  C  =  [_ m  /  k ]_ C )
11469, 113difeq12d 3308 . . . . . . . . . 10  |-  ( k  =  m  ->  ( B  \  C )  =  ( [_ m  / 
k ]_ B  \  [_ m  /  k ]_ C
) )
115112, 114, 69ifbieq12d 3600 . . . . . . . . 9  |-  ( k  =  m  ->  if ( k  =  X ,  ( B  \  C ) ,  B
)  =  if ( m  =  X , 
( [_ m  /  k ]_ B  \  [_ m  /  k ]_ C
) ,  [_ m  /  k ]_ B
) )
11668, 115eleq12d 2364 . . . . . . . 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 2773 . . . . . . 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 3175 . . 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 6839 . . 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 2295 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 1632    e. wcel 1696   A.wral 2556   E.wrex 2557   [_csb 3094    \ cdif 3162    C_ wss 3165   ifcif 3578    Fn wfn 5266   ` cfv 5271   X_cixp 6833
This theorem is referenced by:  ptcld  17323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fn 5274  df-fv 5279  df-ixp 6834
  Copyright terms: Public domain W3C validator