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 ) |
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 ) |