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𝒫AAx
Assertion isf34lem2 AVF:𝒫A𝒫A

Proof

Step Hyp Ref Expression
1 compss.a F=x𝒫AAx
2 difss AxA
3 elpw2g AVAx𝒫AAxA
4 2 3 mpbiri AVAx𝒫A
5 4 adantr AVx𝒫AAx𝒫A
6 5 1 fmptd AVF:𝒫A𝒫A