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	$⊢ \underline{Ⅎ} x A$
	fvmptf.2	$⊢ \underline{Ⅎ} x C$
	fvmptf.3	$⊢ x = A \to B = C$
	fvmptf.4	$⊢ F = (x \in D ⟼ B)$
Assertion	fvmptnf	$⊢ \neg C \in V \to F (A) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		fvmptf.1	$⊢ \underline{Ⅎ} x A$
2		fvmptf.2	$⊢ \underline{Ⅎ} x C$
3		fvmptf.3	$⊢ x = A \to B = C$
4		fvmptf.4	$⊢ F = (x \in D ⟼ B)$
5	4	dmmptss	$⊢ dom F \subseteq D$
6	5	sseli	$⊢ A \in dom F \to A \in D$
7		eqid	$⊢ (x \in D ⟼ I (B)) = (x \in D ⟼ I (B))$
8	4 7	fvmptex	$⊢ F (A) = (x \in D ⟼ I (B)) (A)$
9		fvex	$⊢ I (C) \in V$
10		nfcv	$⊢ \underline{Ⅎ} x I$
11	10 2	nffv	$⊢ \underline{Ⅎ} x I (C)$
12	3	fveq2d	$⊢ x = A \to I (B) = I (C)$
13	1 11 12 7	fvmptf	$⊢ (A \in D \land I (C) \in V) \to (x \in D ⟼ I (B)) (A) = I (C)$
14	9 13	mpan2	$⊢ A \in D \to (x \in D ⟼ I (B)) (A) = I (C)$
15	8 14	syl5eq	$⊢ A \in D \to F (A) = I (C)$
16		fvprc	$⊢ \neg C \in V \to I (C) = \emptyset$
17	15 16	sylan9eq	$⊢ (A \in D \land \neg C \in V) \to F (A) = \emptyset$
18	17	expcom	$⊢ \neg C \in V \to (A \in D \to F (A) = \emptyset)$
19	6 18	syl5	$⊢ \neg C \in V \to (A \in dom F \to F (A) = \emptyset)$
20		ndmfv	$⊢ \neg A \in dom F \to F (A) = \emptyset$
21	19 20	pm2.61d1	$⊢ \neg C \in V \to F (A) = \emptyset$

Metamath Proof Explorer

Theorem fvmptnf

Proof