Metamath Proof Explorer

Theorem fvmptnf

Description: The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses fvmptf.1 ⊢Ⅎ_xA
fvmptf.2 ⊢Ⅎ_xC
fvmptf.3 ⊢x=A→B=C
fvmptf.4 ⊢F=x∈D⟼B
Assertion fvmptnf ⊢¬C∈V→F⁡A=∅

Proof

Step Hyp Ref Expression
1 fvmptf.1 ⊢Ⅎ_xA
2 fvmptf.2 ⊢Ⅎ_xC
3 fvmptf.3 ⊢x=A→B=C
4 fvmptf.4 ⊢F=x∈D⟼B
5 4 dmmptss ⊢dom⁡F⊆D
6 5 sseli ⊢A∈dom⁡F→A∈D
7 eqid ⊢x∈D⟼I⁡B=x∈D⟼I⁡B
8 4 7 fvmptex ⊢F⁡A=x∈D⟼I⁡B⁡A
9 fvex ⊢I⁡C∈V
10 nfcv ⊢Ⅎ_xI
11 10 2 nffv ⊢Ⅎ_xI⁡C
12 3 fveq2d ⊢x=A→I⁡B=I⁡C
13 1 11 12 7 fvmptf ⊢A∈D∧I⁡C∈V→x∈D⟼I⁡B⁡A=I⁡C
14 9 13 mpan2 ⊢A∈D→x∈D⟼I⁡B⁡A=I⁡C
15 8 14 eqtrid ⊢A∈D→F⁡A=I⁡C
16 fvprc ⊢¬C∈V→I⁡C=∅
17 15 16 sylan9eq ⊢A∈D∧¬C∈V→F⁡A=∅
18 17 expcom ⊢¬C∈V→A∈D→F⁡A=∅
19 6 18 syl5 ⊢¬C∈V→A∈dom⁡F→F⁡A=∅
20 ndmfv ⊢¬A∈dom⁡F→F⁡A=∅
21 19 20 pm2.61d1 ⊢¬C∈V→F⁡A=∅