Metamath Proof Explorer

Theorem acsfn1

Description: Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 )
2 ralss ⊢ ( 𝑎 ⊆ 𝑋 → ( ∀ 𝑏 ∈ 𝑎 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ 𝑋 ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
3 1 2 syl ⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( ∀ 𝑏 ∈ 𝑎 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ 𝑋 ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
4 vex ⊢ 𝑏 ∈ V
5 4 snss ⊢ ( 𝑏 ∈ 𝑎 ↔ { 𝑏 } ⊆ 𝑎 )
6 5 imbi1i ⊢ ( ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ↔ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) )
7 6 ralbii ⊢ ( ∀ 𝑏 ∈ 𝑋 ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ↔ ∀ 𝑏 ∈ 𝑋 ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) )
8 3 7 bitrdi ⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( ∀ 𝑏 ∈ 𝑎 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ 𝑋 ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
9 8 rabbiia ⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑎 𝐸 ∈ 𝑎 } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑋 ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) }
10 riinrab ⊢ ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑋 ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) }
11 9 10 eqtr4i ⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑎 𝐸 ∈ 𝑎 } = ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } )
12 mreacs ⊢ ( 𝑋 ∈ 𝑉 → ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )
13 simpll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝐸 ∈ 𝑋 ) → 𝑋 ∈ 𝑉 )
14 simpr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝐸 ∈ 𝑋 ) → 𝐸 ∈ 𝑋 )
15 snssi ⊢ ( 𝑏 ∈ 𝑋 → { 𝑏 } ⊆ 𝑋 )
16 15 ad2antlr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝐸 ∈ 𝑋 ) → { 𝑏 } ⊆ 𝑋 )
17 snfi ⊢ { 𝑏 } ∈ Fin
18 17 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝐸 ∈ 𝑋 ) → { 𝑏 } ∈ Fin )
19 acsfn ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐸 ∈ 𝑋 ) ∧ ( { 𝑏 } ⊆ 𝑋 ∧ { 𝑏 } ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
20 13 14 16 18 19 syl22anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
21 20 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) → ( 𝐸 ∈ 𝑋 → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
22 21 ralimdva ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑏 ∈ 𝑋 𝐸 ∈ 𝑋 → ∀ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
23 22 imp ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ∀ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
24 mreriincl ⊢ ( ( ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) ∧ ∀ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
25 12 23 24 syl2an2r ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
26 11 25 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑋 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )