Metamath Proof Explorer


Theorem isf34lem2

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypothesis compss.a
|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion isf34lem2
|- ( A e. V -> F : ~P A --> ~P A )

Proof

Step Hyp Ref Expression
1 compss.a
 |-  F = ( x e. ~P A |-> ( A \ x ) )
2 difss
 |-  ( A \ x ) C_ A
3 elpw2g
 |-  ( A e. V -> ( ( A \ x ) e. ~P A <-> ( A \ x ) C_ A ) )
4 2 3 mpbiri
 |-  ( A e. V -> ( A \ x ) e. ~P A )
5 4 adantr
 |-  ( ( A e. V /\ x e. ~P A ) -> ( A \ x ) e. ~P A )
6 5 1 fmptd
 |-  ( A e. V -> F : ~P A --> ~P A )