Metamath Proof Explorer

Theorem acsfn2

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

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

Proof

Step Hyp Ref Expression
1 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 )
2 ralss ⊢ ( 𝑎 ⊆ 𝑋 → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ 𝑋 ( 𝑏 ∈ 𝑎 → ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 ) ) )
3 ralss ⊢ ( 𝑎 ⊆ 𝑋 → ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ↔ ∀ 𝑐 ∈ 𝑋 ( 𝑐 ∈ 𝑎 → ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ) ) )
4 r19.21v ⊢ ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ↔ ( 𝑏 ∈ 𝑎 → ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 ) )
5 impexp ⊢ ( ( ( 𝑐 ∈ 𝑎 ∧ 𝑏 ∈ 𝑎 ) → 𝐸 ∈ 𝑎 ) ↔ ( 𝑐 ∈ 𝑎 → ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
6 vex ⊢ 𝑐 ∈ V
7 vex ⊢ 𝑏 ∈ V
8 6 7 prss ⊢ ( ( 𝑐 ∈ 𝑎 ∧ 𝑏 ∈ 𝑎 ) ↔ { 𝑐 , 𝑏 } ⊆ 𝑎 )
9 8 imbi1i ⊢ ( ( ( 𝑐 ∈ 𝑎 ∧ 𝑏 ∈ 𝑎 ) → 𝐸 ∈ 𝑎 ) ↔ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) )
10 5 9 bitr3i ⊢ ( ( 𝑐 ∈ 𝑎 → ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ) ↔ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) )
11 10 ralbii ⊢ ( ∀ 𝑐 ∈ 𝑋 ( 𝑐 ∈ 𝑎 → ( 𝑏 ∈ 𝑎 → 𝐸 ∈ 𝑎 ) ) ↔ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) )
12 3 4 11 3bitr3g ⊢ ( 𝑎 ⊆ 𝑋 → ( ( 𝑏 ∈ 𝑎 → ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 ) ↔ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
13 12 ralbidv ⊢ ( 𝑎 ⊆ 𝑋 → ( ∀ 𝑏 ∈ 𝑋 ( 𝑏 ∈ 𝑎 → ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 ) ↔ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
14 2 13 bitrd ⊢ ( 𝑎 ⊆ 𝑋 → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
15 1 14 syl ⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 ↔ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) ) )
16 15 rabbiia ⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) }
17 riinrab ⊢ ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) }
18 16 17 eqtr4i ⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } = ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } )
19 mreacs ⊢ ( 𝑋 ∈ 𝑉 → ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )
20 riinrab ⊢ ( 𝒫 𝑋 ∩ ∩ 𝑐 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) }
21 19 ad2antrr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )
22 simpll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋 ) ) → 𝑋 ∈ 𝑉 )
23 simprr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋 ) ) → 𝐸 ∈ 𝑋 )
24 prssi ⊢ ( ( 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → { 𝑐 , 𝑏 } ⊆ 𝑋 )
25 24 ancoms ⊢ ( ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) → { 𝑐 , 𝑏 } ⊆ 𝑋 )
26 25 ad2ant2lr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋 ) ) → { 𝑐 , 𝑏 } ⊆ 𝑋 )
27 prfi ⊢ { 𝑐 , 𝑏 } ∈ Fin
28 27 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋 ) ) → { 𝑐 , 𝑏 } ∈ Fin )
29 acsfn ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐸 ∈ 𝑋 ) ∧ ( { 𝑐 , 𝑏 } ⊆ 𝑋 ∧ { 𝑐 , 𝑏 } ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
30 22 23 26 28 29 syl22anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋 ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
31 30 expr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) → ( 𝐸 ∈ 𝑋 → { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
32 31 ralimdva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) → ( ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 → ∀ 𝑐 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
33 32 imp ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ∀ 𝑐 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
34 mreriincl ⊢ ( ( ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) ∧ ∀ 𝑐 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑐 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
35 21 33 34 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ( 𝒫 𝑋 ∩ ∩ 𝑐 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
36 20 35 eqeltrrid ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) ∧ ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
37 36 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑋 ) → ( ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
38 37 ralimdva ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 → ∀ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) )
39 38 imp ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ∀ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
40 mreriincl ⊢ ( ( ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) ∧ ∀ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
41 19 39 40 syl2an2r ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝑋 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑋 ( { 𝑐 , 𝑏 } ⊆ 𝑎 → 𝐸 ∈ 𝑎 ) } ) ∈ ( ACS ‘ 𝑋 ) )
42 18 41 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )