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 if b = T K
2 funiunfv Fun b 𝒫 X if b = T K c 𝒫 a Fin b 𝒫 X if b = T K c = b 𝒫 X if b = T K 𝒫 a Fin
3 1 2 mp1i X V K X T X T Fin a 𝒫 X c 𝒫 a Fin b 𝒫 X if b = T K c = b 𝒫 X if b = T K 𝒫 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 if b = T K = if c = T K
13 eqid b 𝒫 X if b = T K = b 𝒫 X if b = T K
14 snex K V
15 0ex V
16 14 15 ifex if c = T K V
17 12 13 16 fvmpt c 𝒫 X b 𝒫 X if b = T K c = if c = T K
18 10 17 syl X V K X T X T Fin a 𝒫 X c 𝒫 a Fin b 𝒫 X if b = T K c = if c = T K
19 18 iuneq2dv X V K X T X T Fin a 𝒫 X c 𝒫 a Fin b 𝒫 X if b = T K c = c 𝒫 a Fin if c = T K
20 3 19 eqtr3d X V K X T X T Fin a 𝒫 X b 𝒫 X if b = T K 𝒫 a Fin = c 𝒫 a Fin if c = T K
21 20 sseq1d X V K X T X T Fin a 𝒫 X b 𝒫 X if b = T K 𝒫 a Fin a c 𝒫 a Fin if c = T K a
22 iunss c 𝒫 a Fin if c = T K a c 𝒫 a Fin if c = T K a
23 sseq1 K = if c = T K K a if c = T K a
24 23 bibi1d K = if c = T K K a c = T K a if c = T K a c = T K a
25 sseq1 = if c = T K a if c = T K a
26 25 bibi1d = if c = T K a c = T K a if c = T K 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 if c = T K a c = T K a
38 37 ralbidv K X c 𝒫 a Fin if c = T K a c 𝒫 a Fin c = T K a
39 38 ad3antlr X V K X T X T Fin a 𝒫 X c 𝒫 a Fin if c = T K a c 𝒫 a Fin c = T K a
40 22 39 syl5bb X V K X T X T Fin a 𝒫 X c 𝒫 a Fin if c = T K a c 𝒫 a Fin c = 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 Fin c = T K a c 𝒫 X c 𝒫 a Fin c = T K a
46 44 45 syl X V K X T X T Fin a 𝒫 X c 𝒫 a Fin c = T K a c 𝒫 X c 𝒫 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 𝒫 X c 𝒫 a Fin c = T K a c 𝒫 X c = 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 𝒫 X c = 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 𝒫 X c = T c 𝒫 a Fin K a T 𝒫 a Fin K a
56 48 55 syl5bb X V K X T X T Fin a 𝒫 X c 𝒫 X c 𝒫 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 Fin c = 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 if b = T K 𝒫 a Fin a
67 66 rabbidva X V K X T X T Fin a 𝒫 X | T a K a = a 𝒫 X | b 𝒫 X if b = T K 𝒫 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 if b = T K 𝒫 X
73 70 71 72 sylancl X V K X T X T Fin if b = T K 𝒫 X
74 73 adantr X V K X T X T Fin b 𝒫 X if b = T K 𝒫 X
75 74 fmpttd X V K X T X T Fin b 𝒫 X if b = T K : 𝒫 X 𝒫 X
76 isacs1i X V b 𝒫 X if b = T K : 𝒫 X 𝒫 X a 𝒫 X | b 𝒫 X if b = T K 𝒫 a Fin a ACS X
77 68 75 76 syl2anc X V K X T X T Fin a 𝒫 X | b 𝒫 X if b = T K 𝒫 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