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∈V∧K∈X∧T⊆X∧T∈Fin→a∈𝒫X|T⊆a→K∈a∈ACS⁡X

Proof

Step Hyp Ref Expression
1 funmpt ⊢Fun⁡b∈𝒫X⟼ifb=TK∅
2 funiunfv ⊢Fun⁡b∈𝒫X⟼ifb=TK∅→⋃c∈𝒫a∩Finb∈𝒫X⟼ifb=TK∅⁡c=⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin
3 1 2 mp1i ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→⋃c∈𝒫a∩Finb∈𝒫X⟼ifb=TK∅⁡c=⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin
4 elinel1 ⊢c∈𝒫a∩Fin→c∈𝒫a
5 4 elpwid ⊢c∈𝒫a∩Fin→c⊆a
6 elpwi ⊢a∈𝒫X→a⊆X
7 5 6 sylan9ssr ⊢a∈𝒫X∧c∈𝒫a∩Fin→c⊆X
8 velpw ⊢c∈𝒫X↔c⊆X
9 7 8 sylibr ⊢a∈𝒫X∧c∈𝒫a∩Fin→c∈𝒫X
10 9 adantll ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X∧c∈𝒫a∩Fin→c∈𝒫X
11 eqeq1 ⊢b=c→b=T↔c=T
12 11 ifbid ⊢b=c→ifb=TK∅=ifc=TK∅
13 eqid ⊢b∈𝒫X⟼ifb=TK∅=b∈𝒫X⟼ifb=TK∅
14 snex ⊢K∈V
15 0ex ⊢∅∈V
16 14 15 ifex ⊢ifc=TK∅∈V
17 12 13 16 fvmpt ⊢c∈𝒫X→b∈𝒫X⟼ifb=TK∅⁡c=ifc=TK∅
18 10 17 syl ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X∧c∈𝒫a∩Fin→b∈𝒫X⟼ifb=TK∅⁡c=ifc=TK∅
19 18 iuneq2dv ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→⋃c∈𝒫a∩Finb∈𝒫X⟼ifb=TK∅⁡c=⋃c∈𝒫a∩Finifc=TK∅
20 3 19 eqtr3d ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin=⋃c∈𝒫a∩Finifc=TK∅
21 20 sseq1d ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin⊆a↔⋃c∈𝒫a∩Finifc=TK∅⊆a
22 iunss ⊢⋃c∈𝒫a∩Finifc=TK∅⊆a↔∀c∈𝒫a∩Finifc=TK∅⊆a
23 sseq1 ⊢K=ifc=TK∅→K⊆a↔ifc=TK∅⊆a
24 23 bibi1d ⊢K=ifc=TK∅→K⊆a↔c=T→K∈a↔ifc=TK∅⊆a↔c=T→K∈a
25 sseq1 ⊢∅=ifc=TK∅→∅⊆a↔ifc=TK∅⊆a
26 25 bibi1d ⊢∅=ifc=TK∅→∅⊆a↔c=T→K∈a↔ifc=TK∅⊆a↔c=T→K∈a
27 snssg ⊢K∈X→K∈a↔K⊆a
28 27 adantr ⊢K∈X∧c=T→K∈a↔K⊆a
29 biimt ⊢c=T→K∈a↔c=T→K∈a
30 29 adantl ⊢K∈X∧c=T→K∈a↔c=T→K∈a
31 28 30 bitr3d ⊢K∈X∧c=T→K⊆a↔c=T→K∈a
32 0ss ⊢∅⊆a
33 32 a1i ⊢¬c=T→∅⊆a
34 pm2.21 ⊢¬c=T→c=T→K∈a
35 33 34 2thd ⊢¬c=T→∅⊆a↔c=T→K∈a
36 35 adantl ⊢K∈X∧¬c=T→∅⊆a↔c=T→K∈a
37 24 26 31 36 ifbothda ⊢K∈X→ifc=TK∅⊆a↔c=T→K∈a
38 37 ralbidv ⊢K∈X→∀c∈𝒫a∩Finifc=TK∅⊆a↔∀c∈𝒫a∩Finc=T→K∈a
39 38 ad3antlr ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→∀c∈𝒫a∩Finifc=TK∅⊆a↔∀c∈𝒫a∩Finc=T→K∈a
40 22 39 bitrid ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→⋃c∈𝒫a∩Finifc=TK∅⊆a↔∀c∈𝒫a∩Finc=T→K∈a
41 inss1 ⊢𝒫a∩Fin⊆𝒫a
42 6 sspwd ⊢a∈𝒫X→𝒫a⊆𝒫X
43 41 42 sstrid ⊢a∈𝒫X→𝒫a∩Fin⊆𝒫X
44 43 adantl ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→𝒫a∩Fin⊆𝒫X
45 ralss ⊢𝒫a∩Fin⊆𝒫X→∀c∈𝒫a∩Finc=T→K∈a↔∀c∈𝒫Xc∈𝒫a∩Fin→c=T→K∈a
46 44 45 syl ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→∀c∈𝒫a∩Finc=T→K∈a↔∀c∈𝒫Xc∈𝒫a∩Fin→c=T→K∈a
47 bi2.04 ⊢c∈𝒫a∩Fin→c=T→K∈a↔c=T→c∈𝒫a∩Fin→K∈a
48 47 ralbii ⊢∀c∈𝒫Xc∈𝒫a∩Fin→c=T→K∈a↔∀c∈𝒫Xc=T→c∈𝒫a∩Fin→K∈a
49 elpwg ⊢T∈Fin→T∈𝒫X↔T⊆X
50 49 biimparc ⊢T⊆X∧T∈Fin→T∈𝒫X
51 50 ad2antlr ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→T∈𝒫X
52 eleq1 ⊢c=T→c∈𝒫a∩Fin↔T∈𝒫a∩Fin
53 52 imbi1d ⊢c=T→c∈𝒫a∩Fin→K∈a↔T∈𝒫a∩Fin→K∈a
54 53 ceqsralv ⊢T∈𝒫X→∀c∈𝒫Xc=T→c∈𝒫a∩Fin→K∈a↔T∈𝒫a∩Fin→K∈a
55 51 54 syl ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→∀c∈𝒫Xc=T→c∈𝒫a∩Fin→K∈a↔T∈𝒫a∩Fin→K∈a
56 48 55 bitrid ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→∀c∈𝒫Xc∈𝒫a∩Fin→c=T→K∈a↔T∈𝒫a∩Fin→K∈a
57 simplrr ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→T∈Fin
58 57 biantrud ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→T∈𝒫a↔T∈𝒫a∧T∈Fin
59 elin ⊢T∈𝒫a∩Fin↔T∈𝒫a∧T∈Fin
60 58 59 bitr4di ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→T∈𝒫a↔T∈𝒫a∩Fin
61 vex ⊢a∈V
62 61 elpw2 ⊢T∈𝒫a↔T⊆a
63 60 62 bitr3di ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→T∈𝒫a∩Fin↔T⊆a
64 63 imbi1d ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→T∈𝒫a∩Fin→K∈a↔T⊆a→K∈a
65 46 56 64 3bitrd ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→∀c∈𝒫a∩Finc=T→K∈a↔T⊆a→K∈a
66 21 40 65 3bitrrd ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧a∈𝒫X→T⊆a→K∈a↔⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin⊆a
67 66 rabbidva ⊢X∈V∧K∈X∧T⊆X∧T∈Fin→a∈𝒫X|T⊆a→K∈a=a∈𝒫X|⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin⊆a
68 simpll ⊢X∈V∧K∈X∧T⊆X∧T∈Fin→X∈V
69 snelpwi ⊢K∈X→K∈𝒫X
70 69 ad2antlr ⊢X∈V∧K∈X∧T⊆X∧T∈Fin→K∈𝒫X
71 0elpw ⊢∅∈𝒫X
72 ifcl ⊢K∈𝒫X∧∅∈𝒫X→ifb=TK∅∈𝒫X
73 70 71 72 sylancl ⊢X∈V∧K∈X∧T⊆X∧T∈Fin→ifb=TK∅∈𝒫X
74 73 adantr ⊢X∈V∧K∈X∧T⊆X∧T∈Fin∧b∈𝒫X→ifb=TK∅∈𝒫X
75 74 fmpttd ⊢X∈V∧K∈X∧T⊆X∧T∈Fin→b∈𝒫X⟼ifb=TK∅:𝒫X⟶𝒫X
76 isacs1i ⊢X∈V∧b∈𝒫X⟼ifb=TK∅:𝒫X⟶𝒫X→a∈𝒫X|⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin⊆a∈ACS⁡X
77 68 75 76 syl2anc ⊢X∈V∧K∈X∧T⊆X∧T∈Fin→a∈𝒫X|⋃b∈𝒫X⟼ifb=TK∅𝒫a∩Fin⊆a∈ACS⁡X
78 67 77 eqeltrd ⊢X∈V∧K∈X∧T⊆X∧T∈Fin→a∈𝒫X|T⊆a→K∈a∈ACS⁡X