This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acsfn1p

Description: Construction of a closure rule from a one-parameterpartial operation. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion acsfn1p ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 riinrab ⊢ ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) }
2 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
3 2 sseli ⊢ ( 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑏 ∈ 𝑌 )
4 3 biantrud ⊢ ( 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) → ( 𝑏 ∈ 𝑎 ↔ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌 ) ) )
5 vex ⊢ 𝑏 ∈ V
6 5 snss ⊢ ( 𝑏 ∈ 𝑎 ↔ { 𝑏 } ⊆ 𝑎 )
7 6 bicomi ⊢ ( { 𝑏 } ⊆ 𝑎 ↔ 𝑏 ∈ 𝑎 )
8 elin ⊢ ( 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) ↔ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌 ) )
9 4 7 8 3bitr4g ⊢ ( 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) → ( { 𝑏 } ⊆ 𝑎 ↔ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) ) )
10 9 imbi1d ⊢ ( 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ↔ ( 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) → 𝐸 ∈ 𝑎 ) ) )
11 10 ralbiia ⊢ ( ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ↔ ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ( 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) → 𝐸 ∈ 𝑎 ) )
12 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 )
13 12 ssrind ⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑎 ∩ 𝑌 ) ⊆ ( 𝑋 ∩ 𝑌 ) )
14 13 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑎 ∩ 𝑌 ) ⊆ ( 𝑋 ∩ 𝑌 ) )
15 ralss ⊢ ( ( 𝑎 ∩ 𝑌 ) ⊆ ( 𝑋 ∩ 𝑌 ) → ( ∀ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ( 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) → 𝐸 ∈ 𝑎 ) ) )
16 14 15 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ( 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) → 𝐸 ∈ 𝑎 ) ) )
17 11 16 bitr4id ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ↔ ∀ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) 𝐸 ∈ 𝑎 ) )
18 17 rabbidva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) 𝐸 ∈ 𝑎 } )
19 1 18 eqtrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) 𝐸 ∈ 𝑎 } )
20 mreacs ⊢ ( 𝑋 ∈ 𝑉 → ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )
21 20 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) → ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )
22 ssralv ⊢ ( ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 → ( ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) 𝐸 ∈ 𝑋 ) )
23 2 22 ax-mp ⊢ ( ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) 𝐸 ∈ 𝑋 )
24 simpll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝐸 ∈ 𝑋 ) → 𝑋 ∈ 𝑉 )
25 simpr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝐸 ∈ 𝑋 ) → 𝐸 ∈ 𝑋 )
26 inss1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋
27 26 sseli ⊢ ( 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑏 ∈ 𝑋 )
28 27 ad2antlr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝐸 ∈ 𝑋 ) → 𝑏 ∈ 𝑋 )
29 28 snssd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝐸 ∈ 𝑋 ) → { 𝑏 } ⊆ 𝑋 )
30 snfi ⊢ { 𝑏 } ∈ Fin
31 30 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝐸 ∈ 𝑋 ) → { 𝑏 } ∈ Fin )
32 acsfn ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐸 ∈ 𝑋 ) ∧ ( { 𝑏 } ⊆ 𝑋 ∧ { 𝑏 } ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
33 24 25 29 31 32 syl22anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
34 33 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) ) → ( 𝐸 ∈ 𝑋 → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
35 34 ralimdva ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) 𝐸 ∈ 𝑋 → ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
36 23 35 syl5 ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
37 36 imp ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) → ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
38 mreriincl ⊢ ( ( ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) ∧ ∀ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
39 21 37 38 syl2anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ ( 𝑋 ∩ 𝑌 ) { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
40 19 39 eqeltrrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ ( 𝑎 ∩ 𝑌 ) 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )