This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ 𝒫 A ⟼ A ∖ x
Assertion isf34lem2 ⊢ A ∈ V → F : 𝒫 A ⟶ 𝒫 A

Proof

Step Hyp Ref Expression
1 compss.a ⊢ F = x ∈ 𝒫 A ⟼ A ∖ x
2 difss ⊢ A ∖ x ⊆ A
3 elpw2g ⊢ A ∈ V → A ∖ x ∈ 𝒫 A ↔ A ∖ x ⊆ A
4 2 3 mpbiri ⊢ A ∈ V → A ∖ x ∈ 𝒫 A
5 4 adantr ⊢ A ∈ V ∧ x ∈ 𝒫 A → A ∖ x ∈ 𝒫 A
6 5 1 fmptd ⊢ A ∈ V → F : 𝒫 A ⟶ 𝒫 A