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 ( ( 𝑋𝑉𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → { 𝑠 ∈ 𝒫 𝑋 ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∈ ( ACS ‘ 𝑋 ) )

Proof

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