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

Metamath Proof Explorer

Theorem isf34lem1

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

Ref Expression
Hypothesis compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion isf34lem1 ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐴 ∖ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2 difeq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑎 ) )
3 2 cbvmptv ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) ) = ( 𝑎 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑎 ) )
4 1 3 eqtri ⊢ 𝐹 = ( 𝑎 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑎 ) )
5 difeq2 ⊢ ( 𝑎 = 𝑋 → ( 𝐴 ∖ 𝑎 ) = ( 𝐴 ∖ 𝑋 ) )
6 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴 ) )
7 6 biimpar ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ∈ 𝒫 𝐴 )
8 difexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ 𝑋 ) ∈ V )
9 8 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐴 ∖ 𝑋 ) ∈ V )
10 4 5 7 9 fvmptd3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐴 ∖ 𝑋 ) )