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 ) )