Metamath Proof Explorer

Theorem acsfn

Description: Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 funmpt 
 |-  Fun ( b e. ~P X |-> if ( b = T , { K } , (/) ) )
2 funiunfv 
 |-  ( 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 ) ) )
3 1 2 mp1i 
 |-  ( ( ( ( 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 elinel1 
 |-  ( c e. ( ~P a i^i Fin ) -> c e. ~P a )
5 4 elpwid 
 |-  ( c e. ( ~P a i^i Fin ) -> c C_ a )
6 elpwi 
 |-  ( a e. ~P X -> a C_ X )
7 5 6 sylan9ssr 
 |-  ( ( a e. ~P X /\ c e. ( ~P a i^i Fin ) ) -> c C_ X )
8 velpw 
 |-  ( c e. ~P X <-> c C_ X )
9 7 8 sylibr 
 |-  ( ( a e. ~P X /\ c e. ( ~P a i^i Fin ) ) -> c e. ~P X )
10 9 adantll 
 |-  ( ( ( ( ( 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 )
11 eqeq1 
 |-  ( b = c -> ( b = T <-> c = T ) )
12 11 ifbid 
 |-  ( b = c -> if ( b = T , { K } , (/) ) = if ( c = T , { K } , (/) ) )
13 eqid 
 |-  ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) = ( b e. ~P X |-> if ( b = T , { K } , (/) ) )
14 snex 
 |-  { K } e. _V
15 0ex 
 |-  (/) e. _V
16 14 15 ifex 
 |-  if ( c = T , { K } , (/) ) e. _V
17 12 13 16 fvmpt 
 |-  ( c e. ~P X -> ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) ` c ) = if ( c = T , { K } , (/) ) )
18 10 17 syl 
 |-  ( ( ( ( ( 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 } , (/) ) )
19 18 iuneq2dv 
 |-  ( ( ( ( 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 } , (/) ) )
20 3 19 eqtr3d 
 |-  ( ( ( ( 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 } , (/) ) )
21 20 sseq1d 
 |-  ( ( ( ( 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 ) )
22 iunss 
 |-  ( 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 )
23 sseq1 
 |-  ( { K } = if ( c = T , { K } , (/) ) -> ( { K } C_ a <-> if ( c = T , { K } , (/) ) C_ a ) )
24 23 bibi1d 
 |-  ( { K } = if ( c = T , { K } , (/) ) -> ( ( { K } C_ a <-> ( c = T -> K e. a ) ) <-> ( if ( c = T , { K } , (/) ) C_ a <-> ( c = T -> K e. a ) ) ) )
25 sseq1 
 |-  ( (/) = if ( c = T , { K } , (/) ) -> ( (/) C_ a <-> if ( c = T , { K } , (/) ) C_ a ) )
26 25 bibi1d 
 |-  ( (/) = if ( c = T , { K } , (/) ) -> ( ( (/) C_ a <-> ( c = T -> K e. a ) ) <-> ( if ( c = T , { K } , (/) ) C_ a <-> ( c = T -> K e. a ) ) ) )
27 snssg 
 |-  ( K e. X -> ( K e. a <-> { K } C_ a ) )
28 27 adantr 
 |-  ( ( K e. X /\ c = T ) -> ( K e. a <-> { K } C_ a ) )
29 biimt 
 |-  ( c = T -> ( K e. a <-> ( c = T -> K e. a ) ) )
30 29 adantl 
 |-  ( ( K e. X /\ c = T ) -> ( K e. a <-> ( c = T -> K e. a ) ) )
31 28 30 bitr3d 
 |-  ( ( K e. X /\ c = T ) -> ( { K } C_ a <-> ( c = T -> K e. a ) ) )
32 0ss 
 |-  (/) C_ a
33 32 a1i 
 |-  ( -. c = T -> (/) C_ a )
34 pm2.21 
 |-  ( -. c = T -> ( c = T -> K e. a ) )
35 33 34 2thd 
 |-  ( -. c = T -> ( (/) C_ a <-> ( c = T -> K e. a ) ) )
36 35 adantl 
 |-  ( ( K e. X /\ -. c = T ) -> ( (/) C_ a <-> ( c = T -> K e. a ) ) )
37 24 26 31 36 ifbothda 
 |-  ( K e. X -> ( if ( c = T , { K } , (/) ) C_ a <-> ( c = T -> K e. a ) ) )
38 37 ralbidv 
 |-  ( 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 ) ) )
39 38 ad3antlr 
 |-  ( ( ( ( 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 ) ) )
40 22 39 syl5bb 
 |-  ( ( ( ( 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 ) ) )
41 inss1 
 |-  ( ~P a i^i Fin ) C_ ~P a
42 6 sspwd 
 |-  ( a e. ~P X -> ~P a C_ ~P X )
43 41 42 sstrid 
 |-  ( a e. ~P X -> ( ~P a i^i Fin ) C_ ~P X )
44 43 adantl 
 |-  ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( ~P a i^i Fin ) C_ ~P X )
45 ralss 
 |-  ( ( ~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 ) ) ) )
46 44 45 syl 
 |-  ( ( ( ( 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 ) ) ) )
47 bi2.04 
 |-  ( ( c e. ( ~P a i^i Fin ) -> ( c = T -> K e. a ) ) <-> ( c = T -> ( c e. ( ~P a i^i Fin ) -> K e. a ) ) )
48 47 ralbii 
 |-  ( 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 ) ) )
49 elpwg 
 |-  ( T e. Fin -> ( T e. ~P X <-> T C_ X ) )
50 49 biimparc 
 |-  ( ( T C_ X /\ T e. Fin ) -> T e. ~P X )
51 50 ad2antlr 
 |-  ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> T e. ~P X )
52 eleq1 
 |-  ( c = T -> ( c e. ( ~P a i^i Fin ) <-> T e. ( ~P a i^i Fin ) ) )
53 52 imbi1d 
 |-  ( c = T -> ( ( c e. ( ~P a i^i Fin ) -> K e. a ) <-> ( T e. ( ~P a i^i Fin ) -> K e. a ) ) )
54 53 ceqsralv 
 |-  ( 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 ) ) )
55 51 54 syl 
 |-  ( ( ( ( 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 ) ) )
56 48 55 syl5bb 
 |-  ( ( ( ( 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 ) ) )
57 simplrr 
 |-  ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> T e. Fin )
58 57 biantrud 
 |-  ( ( ( ( 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 ) ) )
59 elin 
 |-  ( T e. ( ~P a i^i Fin ) <-> ( T e. ~P a /\ T e. Fin ) )
60 58 59 bitr4di 
 |-  ( ( ( ( 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 ) ) )
61 vex 
 |-  a e. _V
62 61 elpw2 
 |-  ( T e. ~P a <-> T C_ a )
63 60 62 bitr3di 
 |-  ( ( ( ( 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 ) )
64 63 imbi1d 
 |-  ( ( ( ( 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 ) ) )
65 46 56 64 3bitrd 
 |-  ( ( ( ( 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 ) ) )
66 21 40 65 3bitrrd 
 |-  ( ( ( ( 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 ) )
67 66 rabbidva 
 |-  ( ( ( 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 } )
68 simpll 
 |-  ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> X e. V )
69 snelpwi 
 |-  ( K e. X -> { K } e. ~P X )
70 69 ad2antlr 
 |-  ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> { K } e. ~P X )
71 0elpw 
 |-  (/) e. ~P X
72 ifcl 
 |-  ( ( { K } e. ~P X /\ (/) e. ~P X ) -> if ( b = T , { K } , (/) ) e. ~P X )
73 70 71 72 sylancl 
 |-  ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> if ( b = T , { K } , (/) ) e. ~P X )
74 73 adantr 
 |-  ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ b e. ~P X ) -> if ( b = T , { K } , (/) ) e. ~P X )
75 74 fmpttd 
 |-  ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) : ~P X --> ~P X )
76 isacs1i 
 |-  ( ( 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 ) )
77 68 75 76 syl2anc 
 |-  ( ( ( 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 ) )
78 67 77 eqeltrd 
 |-  ( ( ( 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 ) )