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

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 ⊢ Ⅎ _ x A
fvmptf.2 ⊢ Ⅎ _ x C
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 ⊢ Ⅎ _ x A
2 fvmptf.2 ⊢ Ⅎ _ x C
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 ⊢ Ⅎ _ x I
11 10 2 nffv ⊢ Ⅎ _ x I ⁡ 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 = ∅