Metamath Proof Explorer

Theorem fival

Description: The set of all the finite intersections of the elements of A . (Contributed by FL, 27-Apr-2008) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fival 
|- ( A e. V -> ( fi ` A ) = { y | E. x e. ( ~P A i^i Fin ) y = |^| x } )

Proof

Step Hyp Ref Expression
1 df-fi 
 |-  fi = ( z e. _V |-> { y | E. x e. ( ~P z i^i Fin ) y = |^| x } )
2 pweq 
 |-  ( z = A -> ~P z = ~P A )
3 2 ineq1d 
 |-  ( z = A -> ( ~P z i^i Fin ) = ( ~P A i^i Fin ) )
4 3 rexeqdv 
 |-  ( z = A -> ( E. x e. ( ~P z i^i Fin ) y = |^| x <-> E. x e. ( ~P A i^i Fin ) y = |^| x ) )
5 4 abbidv 
 |-  ( z = A -> { y | E. x e. ( ~P z i^i Fin ) y = |^| x } = { y | E. x e. ( ~P A i^i Fin ) y = |^| x } )
6 elex 
 |-  ( A e. V -> A e. _V )
7 simpr 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> y = |^| x )
8 elinel1 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
9 8 elpwid 
 |-  ( x e. ( ~P A i^i Fin ) -> x C_ A )
10 eqvisset 
 |-  ( y = |^| x -> |^| x e. _V )
11 intex 
 |-  ( x =/= (/) <-> |^| x e. _V )
12 10 11 sylibr 
 |-  ( y = |^| x -> x =/= (/) )
13 intssuni2 
 |-  ( ( x C_ A /\ x =/= (/) ) -> |^| x C_ U. A )
14 9 12 13 syl2an 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> |^| x C_ U. A )
15 7 14 eqsstrd 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> y C_ U. A )
16 velpw 
 |-  ( y e. ~P U. A <-> y C_ U. A )
17 15 16 sylibr 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> y e. ~P U. A )
18 17 rexlimiva 
 |-  ( E. x e. ( ~P A i^i Fin ) y = |^| x -> y e. ~P U. A )
19 18 abssi 
 |-  { y | E. x e. ( ~P A i^i Fin ) y = |^| x } C_ ~P U. A
20 uniexg 
 |-  ( A e. V -> U. A e. _V )
21 20 pwexd 
 |-  ( A e. V -> ~P U. A e. _V )
22 ssexg 
 |-  ( ( { y | E. x e. ( ~P A i^i Fin ) y = |^| x } C_ ~P U. A /\ ~P U. A e. _V ) -> { y | E. x e. ( ~P A i^i Fin ) y = |^| x } e. _V )
23 19 21 22 sylancr 
 |-  ( A e. V -> { y | E. x e. ( ~P A i^i Fin ) y = |^| x } e. _V )
24 1 5 6 23 fvmptd3 
 |-  ( A e. V -> ( fi ` A ) = { y | E. x e. ( ~P A i^i Fin ) y = |^| x } )