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

Theorem acsfn 13847
Description: Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
Assertion
Ref Expression
acsfn  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  ->  { a  e.  ~P X  |  ( T  C_  a  ->  K  e.  a ) }  e.  (ACS `  X ) )
Distinct variable groups:    K, a    T, a    V, a    X, a

Proof of Theorem acsfn
Dummy variables  b 
c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funmpt 5456 . . . . . . 7  |-  Fun  (
b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )
2 funiunfv 5962 . . . . . . 7  |-  ( Fun  ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )  ->  U_ c  e.  ( ~P a  i^i  Fin ) ( ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) `  c )  =  U. ( ( b  e. 
~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) " ( ~P a  i^i  Fin )
) )
31, 2mp1i 12 . . . . . 6  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  U_ c  e.  ( ~P a  i^i 
Fin ) ( ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) `
 c )  = 
U. ( ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) "
( ~P a  i^i 
Fin ) ) )
4 inss1 3529 . . . . . . . . . . . . 13  |-  ( ~P a  i^i  Fin )  C_ 
~P a
54sseli 3312 . . . . . . . . . . . 12  |-  ( c  e.  ( ~P a  i^i  Fin )  ->  c  e.  ~P a )
65elpwid 3776 . . . . . . . . . . 11  |-  ( c  e.  ( ~P a  i^i  Fin )  ->  c  C_  a )
7 elpwi 3775 . . . . . . . . . . 11  |-  ( a  e.  ~P X  -> 
a  C_  X )
86, 7sylan9ssr 3330 . . . . . . . . . 10  |-  ( ( a  e.  ~P X  /\  c  e.  ( ~P a  i^i  Fin )
)  ->  c  C_  X )
9 vex 2927 . . . . . . . . . . 11  |-  c  e. 
_V
109elpw 3773 . . . . . . . . . 10  |-  ( c  e.  ~P X  <->  c  C_  X )
118, 10sylibr 204 . . . . . . . . 9  |-  ( ( a  e.  ~P X  /\  c  e.  ( ~P a  i^i  Fin )
)  ->  c  e.  ~P X )
1211adantll 695 . . . . . . . 8  |-  ( ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  /\  c  e.  ( ~P a  i^i  Fin ) )  ->  c  e.  ~P X )
13 eqeq1 2418 . . . . . . . . . 10  |-  ( b  =  c  ->  (
b  =  T  <->  c  =  T ) )
1413ifbid 3725 . . . . . . . . 9  |-  ( b  =  c  ->  if ( b  =  T ,  { K } ,  (/) )  =  if ( c  =  T ,  { K } ,  (/) ) )
15 eqid 2412 . . . . . . . . 9  |-  ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )  =  ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )
16 snex 4373 . . . . . . . . . 10  |-  { K }  e.  _V
17 0ex 4307 . . . . . . . . . 10  |-  (/)  e.  _V
1816, 17ifex 3765 . . . . . . . . 9  |-  if ( c  =  T ,  { K } ,  (/) )  e.  _V
1914, 15, 18fvmpt 5773 . . . . . . . 8  |-  ( c  e.  ~P X  -> 
( ( b  e. 
~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) `  c
)  =  if ( c  =  T ,  { K } ,  (/) ) )
2012, 19syl 16 . . . . . . 7  |-  ( ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  /\  c  e.  ( ~P a  i^i  Fin ) )  ->  (
( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) `
 c )  =  if ( c  =  T ,  { K } ,  (/) ) )
2120iuneq2dv 4082 . . . . . 6  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  U_ c  e.  ( ~P a  i^i 
Fin ) ( ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) `
 c )  = 
U_ c  e.  ( ~P a  i^i  Fin ) if ( c  =  T ,  { K } ,  (/) ) )
223, 21eqtr3d 2446 . . . . 5  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  U. (
( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )
" ( ~P a  i^i  Fin ) )  = 
U_ c  e.  ( ~P a  i^i  Fin ) if ( c  =  T ,  { K } ,  (/) ) )
2322sseq1d 3343 . . . 4  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( U. ( ( b  e. 
~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) " ( ~P a  i^i  Fin )
)  C_  a  <->  U_ c  e.  ( ~P a  i^i 
Fin ) if ( c  =  T ,  { K } ,  (/) )  C_  a ) )
24 iunss 4100 . . . . 5  |-  ( U_ c  e.  ( ~P a  i^i  Fin ) if ( c  =  T ,  { K } ,  (/) )  C_  a  <->  A. c  e.  ( ~P a  i^i  Fin ) if ( c  =  T ,  { K } ,  (/) )  C_  a
)
25 sseq1 3337 . . . . . . . . 9  |-  ( { K }  =  if ( c  =  T ,  { K } ,  (/) )  ->  ( { K }  C_  a  <->  if ( c  =  T ,  { K } ,  (/) )  C_  a
) )
2625bibi1d 311 . . . . . . . 8  |-  ( { K }  =  if ( c  =  T ,  { K } ,  (/) )  ->  (
( { K }  C_  a  <->  ( c  =  T  ->  K  e.  a ) )  <->  ( if ( c  =  T ,  { K } ,  (/) )  C_  a  <->  ( c  =  T  ->  K  e.  a )
) ) )
27 sseq1 3337 . . . . . . . . 9  |-  ( (/)  =  if ( c  =  T ,  { K } ,  (/) )  -> 
( (/)  C_  a  <->  if (
c  =  T ,  { K } ,  (/) )  C_  a ) )
2827bibi1d 311 . . . . . . . 8  |-  ( (/)  =  if ( c  =  T ,  { K } ,  (/) )  -> 
( ( (/)  C_  a  <->  ( c  =  T  ->  K  e.  a )
)  <->  ( if ( c  =  T ,  { K } ,  (/) )  C_  a  <->  ( c  =  T  ->  K  e.  a ) ) ) )
29 snssg 3900 . . . . . . . . . 10  |-  ( K  e.  X  ->  ( K  e.  a  <->  { K }  C_  a ) )
3029adantr 452 . . . . . . . . 9  |-  ( ( K  e.  X  /\  c  =  T )  ->  ( K  e.  a  <->  { K }  C_  a
) )
31 biimt 326 . . . . . . . . . 10  |-  ( c  =  T  ->  ( K  e.  a  <->  ( c  =  T  ->  K  e.  a ) ) )
3231adantl 453 . . . . . . . . 9  |-  ( ( K  e.  X  /\  c  =  T )  ->  ( K  e.  a  <-> 
( c  =  T  ->  K  e.  a ) ) )
3330, 32bitr3d 247 . . . . . . . 8  |-  ( ( K  e.  X  /\  c  =  T )  ->  ( { K }  C_  a  <->  ( c  =  T  ->  K  e.  a ) ) )
34 0ss 3624 . . . . . . . . . . 11  |-  (/)  C_  a
3534a1i 11 . . . . . . . . . 10  |-  ( -.  c  =  T  ->  (/)  C_  a )
36 pm2.21 102 . . . . . . . . . 10  |-  ( -.  c  =  T  -> 
( c  =  T  ->  K  e.  a ) )
3735, 362thd 232 . . . . . . . . 9  |-  ( -.  c  =  T  -> 
( (/)  C_  a  <->  ( c  =  T  ->  K  e.  a ) ) )
3837adantl 453 . . . . . . . 8  |-  ( ( K  e.  X  /\  -.  c  =  T
)  ->  ( (/)  C_  a  <->  ( c  =  T  ->  K  e.  a )
) )
3926, 28, 33, 38ifbothda 3737 . . . . . . 7  |-  ( K  e.  X  ->  ( if ( c  =  T ,  { K } ,  (/) )  C_  a  <->  ( c  =  T  ->  K  e.  a )
) )
4039ralbidv 2694 . . . . . 6  |-  ( K  e.  X  ->  ( A. c  e.  ( ~P a  i^i  Fin ) if ( c  =  T ,  { K } ,  (/) )  C_  a  <->  A. c  e.  ( ~P a  i^i  Fin )
( c  =  T  ->  K  e.  a ) ) )
4140ad3antlr 712 . . . . 5  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( A. c  e.  ( ~P a  i^i  Fin ) if ( c  =  T ,  { K } ,  (/) )  C_  a  <->  A. c  e.  ( ~P a  i^i  Fin )
( c  =  T  ->  K  e.  a ) ) )
4224, 41syl5bb 249 . . . 4  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( U_ c  e.  ( ~P a  i^i  Fin ) if ( c  =  T ,  { K } ,  (/) )  C_  a  <->  A. c  e.  ( ~P a  i^i  Fin )
( c  =  T  ->  K  e.  a ) ) )
43 sspwb 4381 . . . . . . . . 9  |-  ( a 
C_  X  <->  ~P a  C_ 
~P X )
447, 43sylib 189 . . . . . . . 8  |-  ( a  e.  ~P X  ->  ~P a  C_  ~P X
)
454, 44syl5ss 3327 . . . . . . 7  |-  ( a  e.  ~P X  -> 
( ~P a  i^i 
Fin )  C_  ~P X )
4645adantl 453 . . . . . 6  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( ~P a  i^i  Fin )  C_  ~P X )
47 ralss 3377 . . . . . 6  |-  ( ( ~P a  i^i  Fin )  C_  ~P X  -> 
( A. c  e.  ( ~P a  i^i 
Fin ) ( c  =  T  ->  K  e.  a )  <->  A. c  e.  ~P  X ( c  e.  ( ~P a  i^i  Fin )  ->  (
c  =  T  ->  K  e.  a )
) ) )
4846, 47syl 16 . . . . 5  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( A. c  e.  ( ~P a  i^i  Fin ) ( c  =  T  ->  K  e.  a )  <->  A. c  e.  ~P  X
( c  e.  ( ~P a  i^i  Fin )  ->  ( c  =  T  ->  K  e.  a ) ) ) )
49 bi2.04 351 . . . . . . 7  |-  ( ( c  e.  ( ~P a  i^i  Fin )  ->  ( c  =  T  ->  K  e.  a ) )  <->  ( c  =  T  ->  ( c  e.  ( ~P a  i^i  Fin )  ->  K  e.  a ) ) )
5049ralbii 2698 . . . . . 6  |-  ( A. c  e.  ~P  X
( c  e.  ( ~P a  i^i  Fin )  ->  ( c  =  T  ->  K  e.  a ) )  <->  A. c  e.  ~P  X ( c  =  T  ->  (
c  e.  ( ~P a  i^i  Fin )  ->  K  e.  a ) ) )
51 elpwg 3774 . . . . . . . . 9  |-  ( T  e.  Fin  ->  ( T  e.  ~P X  <->  T 
C_  X ) )
5251biimparc 474 . . . . . . . 8  |-  ( ( T  C_  X  /\  T  e.  Fin )  ->  T  e.  ~P X
)
5352ad2antlr 708 . . . . . . 7  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  T  e.  ~P X )
54 eleq1 2472 . . . . . . . . 9  |-  ( c  =  T  ->  (
c  e.  ( ~P a  i^i  Fin )  <->  T  e.  ( ~P a  i^i  Fin ) ) )
5554imbi1d 309 . . . . . . . 8  |-  ( c  =  T  ->  (
( c  e.  ( ~P a  i^i  Fin )  ->  K  e.  a )  <->  ( T  e.  ( ~P a  i^i 
Fin )  ->  K  e.  a ) ) )
5655ceqsralv 2951 . . . . . . 7  |-  ( T  e.  ~P X  -> 
( A. c  e. 
~P  X ( c  =  T  ->  (
c  e.  ( ~P a  i^i  Fin )  ->  K  e.  a ) )  <->  ( T  e.  ( ~P a  i^i 
Fin )  ->  K  e.  a ) ) )
5753, 56syl 16 . . . . . 6  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( A. c  e.  ~P  X
( c  =  T  ->  ( c  e.  ( ~P a  i^i 
Fin )  ->  K  e.  a ) )  <->  ( T  e.  ( ~P a  i^i 
Fin )  ->  K  e.  a ) ) )
5850, 57syl5bb 249 . . . . 5  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( A. c  e.  ~P  X
( c  e.  ( ~P a  i^i  Fin )  ->  ( c  =  T  ->  K  e.  a ) )  <->  ( T  e.  ( ~P a  i^i 
Fin )  ->  K  e.  a ) ) )
59 vex 2927 . . . . . . . 8  |-  a  e. 
_V
6059elpw2 4332 . . . . . . 7  |-  ( T  e.  ~P a  <->  T  C_  a
)
61 simplrr 738 . . . . . . . . 9  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  T  e.  Fin )
6261biantrud 494 . . . . . . . 8  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( T  e.  ~P a  <->  ( T  e.  ~P a  /\  T  e.  Fin ) ) )
63 elin 3498 . . . . . . . 8  |-  ( T  e.  ( ~P a  i^i  Fin )  <->  ( T  e.  ~P a  /\  T  e.  Fin ) )
6462, 63syl6bbr 255 . . . . . . 7  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( T  e.  ~P a  <->  T  e.  ( ~P a  i^i  Fin ) ) )
6560, 64syl5rbbr 252 . . . . . 6  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( T  e.  ( ~P a  i^i 
Fin )  <->  T  C_  a
) )
6665imbi1d 309 . . . . 5  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( ( T  e.  ( ~P a  i^i  Fin )  ->  K  e.  a )  <->  ( T  C_  a  ->  K  e.  a ) ) )
6748, 58, 663bitrd 271 . . . 4  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( A. c  e.  ( ~P a  i^i  Fin ) ( c  =  T  ->  K  e.  a )  <->  ( T  C_  a  ->  K  e.  a ) ) )
6823, 42, 673bitrrd 272 . . 3  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  a  e.  ~P X
)  ->  ( ( T  C_  a  ->  K  e.  a )  <->  U. (
( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )
" ( ~P a  i^i  Fin ) )  C_  a ) )
6968rabbidva 2915 . 2  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  ->  { a  e.  ~P X  |  ( T  C_  a  ->  K  e.  a ) }  =  { a  e.  ~P X  |  U. (
( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )
" ( ~P a  i^i  Fin ) )  C_  a } )
70 simpll 731 . . 3  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  ->  X  e.  V )
71 snelpwi 4377 . . . . . . 7  |-  ( K  e.  X  ->  { K }  e.  ~P X
)
7271ad2antlr 708 . . . . . 6  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  ->  { K }  e.  ~P X )
73 0elpw 4337 . . . . . 6  |-  (/)  e.  ~P X
74 ifcl 3743 . . . . . 6  |-  ( ( { K }  e.  ~P X  /\  (/)  e.  ~P X )  ->  if ( b  =  T ,  { K } ,  (/) )  e.  ~P X )
7572, 73, 74sylancl 644 . . . . 5  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  ->  if ( b  =  T ,  { K } ,  (/) )  e.  ~P X )
7675adantr 452 . . . 4  |-  ( ( ( ( X  e.  V  /\  K  e.  X )  /\  ( T  C_  X  /\  T  e.  Fin ) )  /\  b  e.  ~P X
)  ->  if (
b  =  T ,  { K } ,  (/) )  e.  ~P X
)
7776, 15fmptd 5860 . . 3  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  -> 
( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) : ~P X --> ~P X
)
78 isacs1i 13845 . . 3  |-  ( ( X  e.  V  /\  ( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) : ~P X --> ~P X
)  ->  { a  e.  ~P X  |  U. ( ( b  e. 
~P X  |->  if ( b  =  T ,  { K } ,  (/) ) ) " ( ~P a  i^i  Fin )
)  C_  a }  e.  (ACS `  X )
)
7970, 77, 78syl2anc 643 . 2  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  ->  { a  e.  ~P X  |  U. (
( b  e.  ~P X  |->  if ( b  =  T ,  { K } ,  (/) ) )
" ( ~P a  i^i  Fin ) )  C_  a }  e.  (ACS `  X ) )
8069, 79eqeltrd 2486 1  |-  ( ( ( X  e.  V  /\  K  e.  X
)  /\  ( T  C_  X  /\  T  e. 
Fin ) )  ->  { a  e.  ~P X  |  ( T  C_  a  ->  K  e.  a ) }  e.  (ACS `  X ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2674   {crab 2678    i^i cin 3287    C_ wss 3288   (/)c0 3596   ifcif 3707   ~Pcpw 3767   {csn 3782   U.cuni 3983   U_ciun 4061    e. cmpt 4234   "cima 4848   Fun wfun 5415   -->wf 5417   ` cfv 5421   Fincfn 7076  ACScacs 13773
This theorem is referenced by:  acsfn0  13848  acsfn1  13849  acsfn2  13851  acsfn1p  27383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-mre 13774  df-acs 13777
  Copyright terms: Public domain W3C validator