Metamath Proof Explorer


Theorem isacs1i

Description: A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion isacs1i X V F : 𝒫 X 𝒫 X s 𝒫 X | F 𝒫 s Fin s ACS X

Proof

Step Hyp Ref Expression
1 ssrab2 s 𝒫 X | F 𝒫 s Fin s 𝒫 X
2 1 a1i X V F : 𝒫 X 𝒫 X s 𝒫 X | F 𝒫 s Fin s 𝒫 X
3 pweq s = X t 𝒫 s = 𝒫 X t
4 3 ineq1d s = X t 𝒫 s Fin = 𝒫 X t Fin
5 4 imaeq2d s = X t F 𝒫 s Fin = F 𝒫 X t Fin
6 5 unieqd s = X t F 𝒫 s Fin = F 𝒫 X t Fin
7 id s = X t s = X t
8 6 7 sseq12d s = X t F 𝒫 s Fin s F 𝒫 X t Fin X t
9 inss1 X t X
10 elpw2g X V X t 𝒫 X X t X
11 9 10 mpbiri X V X t 𝒫 X
12 11 ad2antrr X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s X t 𝒫 X
13 imassrn F 𝒫 X t Fin ran F
14 frn F : 𝒫 X 𝒫 X ran F 𝒫 X
15 14 adantl X V F : 𝒫 X 𝒫 X ran F 𝒫 X
16 13 15 sstrid X V F : 𝒫 X 𝒫 X F 𝒫 X t Fin 𝒫 X
17 16 unissd X V F : 𝒫 X 𝒫 X F 𝒫 X t Fin 𝒫 X
18 unipw 𝒫 X = X
19 17 18 sseqtrdi X V F : 𝒫 X 𝒫 X F 𝒫 X t Fin X
20 19 adantr X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 X t Fin X
21 inss2 X t t
22 intss1 a t t a
23 21 22 sstrid a t X t a
24 23 adantl X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t X t a
25 24 sspwd X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t 𝒫 X t 𝒫 a
26 25 ssrind X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t 𝒫 X t Fin 𝒫 a Fin
27 imass2 𝒫 X t Fin 𝒫 a Fin F 𝒫 X t Fin F 𝒫 a Fin
28 26 27 syl X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t F 𝒫 X t Fin F 𝒫 a Fin
29 28 unissd X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t F 𝒫 X t Fin F 𝒫 a Fin
30 ssel2 t s 𝒫 X | F 𝒫 s Fin s a t a s 𝒫 X | F 𝒫 s Fin s
31 pweq s = a 𝒫 s = 𝒫 a
32 31 ineq1d s = a 𝒫 s Fin = 𝒫 a Fin
33 32 imaeq2d s = a F 𝒫 s Fin = F 𝒫 a Fin
34 33 unieqd s = a F 𝒫 s Fin = F 𝒫 a Fin
35 id s = a s = a
36 34 35 sseq12d s = a F 𝒫 s Fin s F 𝒫 a Fin a
37 36 elrab a s 𝒫 X | F 𝒫 s Fin s a 𝒫 X F 𝒫 a Fin a
38 37 simprbi a s 𝒫 X | F 𝒫 s Fin s F 𝒫 a Fin a
39 30 38 syl t s 𝒫 X | F 𝒫 s Fin s a t F 𝒫 a Fin a
40 39 adantll X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t F 𝒫 a Fin a
41 29 40 sstrd X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t F 𝒫 X t Fin a
42 41 ralrimiva X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s a t F 𝒫 X t Fin a
43 ssint F 𝒫 X t Fin t a t F 𝒫 X t Fin a
44 42 43 sylibr X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 X t Fin t
45 20 44 ssind X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 X t Fin X t
46 8 12 45 elrabd X V F : 𝒫 X 𝒫 X t s 𝒫 X | F 𝒫 s Fin s X t s 𝒫 X | F 𝒫 s Fin s
47 2 46 ismred2 X V F : 𝒫 X 𝒫 X s 𝒫 X | F 𝒫 s Fin s Moore X
48 fssxp F : 𝒫 X 𝒫 X F 𝒫 X × 𝒫 X
49 pwexg X V 𝒫 X V
50 49 49 xpexd X V 𝒫 X × 𝒫 X V
51 ssexg F 𝒫 X × 𝒫 X 𝒫 X × 𝒫 X V F V
52 48 50 51 syl2anr X V F : 𝒫 X 𝒫 X F V
53 simpr X V F : 𝒫 X 𝒫 X F : 𝒫 X 𝒫 X
54 pweq s = t 𝒫 s = 𝒫 t
55 54 ineq1d s = t 𝒫 s Fin = 𝒫 t Fin
56 55 imaeq2d s = t F 𝒫 s Fin = F 𝒫 t Fin
57 56 unieqd s = t F 𝒫 s Fin = F 𝒫 t Fin
58 id s = t s = t
59 57 58 sseq12d s = t F 𝒫 s Fin s F 𝒫 t Fin t
60 59 elrab3 t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 t Fin t
61 60 rgen t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 t Fin t
62 53 61 jctir X V F : 𝒫 X 𝒫 X F : 𝒫 X 𝒫 X t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 t Fin t
63 feq1 f = F f : 𝒫 X 𝒫 X F : 𝒫 X 𝒫 X
64 imaeq1 f = F f 𝒫 t Fin = F 𝒫 t Fin
65 64 unieqd f = F f 𝒫 t Fin = F 𝒫 t Fin
66 65 sseq1d f = F f 𝒫 t Fin t F 𝒫 t Fin t
67 66 bibi2d f = F t s 𝒫 X | F 𝒫 s Fin s f 𝒫 t Fin t t s 𝒫 X | F 𝒫 s Fin s F 𝒫 t Fin t
68 67 ralbidv f = F t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s f 𝒫 t Fin t t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 t Fin t
69 63 68 anbi12d f = F f : 𝒫 X 𝒫 X t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s f 𝒫 t Fin t F : 𝒫 X 𝒫 X t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s F 𝒫 t Fin t
70 52 62 69 spcedv X V F : 𝒫 X 𝒫 X f f : 𝒫 X 𝒫 X t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s f 𝒫 t Fin t
71 isacs s 𝒫 X | F 𝒫 s Fin s ACS X s 𝒫 X | F 𝒫 s Fin s Moore X f f : 𝒫 X 𝒫 X t 𝒫 X t s 𝒫 X | F 𝒫 s Fin s f 𝒫 t Fin t
72 47 70 71 sylanbrc X V F : 𝒫 X 𝒫 X s 𝒫 X | F 𝒫 s Fin s ACS X