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 𝑥 𝐴
fvmptf.2 𝑥 𝐶
fvmptf.3 ( 𝑥 = 𝐴𝐵 = 𝐶 )
fvmptf.4 𝐹 = ( 𝑥𝐷𝐵 )
Assertion fvmptnf ( ¬ 𝐶 ∈ V → ( 𝐹𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 fvmptf.1 𝑥 𝐴
2 fvmptf.2 𝑥 𝐶
3 fvmptf.3 ( 𝑥 = 𝐴𝐵 = 𝐶 )
4 fvmptf.4 𝐹 = ( 𝑥𝐷𝐵 )
5 4 dmmptss dom 𝐹𝐷
6 5 sseli ( 𝐴 ∈ dom 𝐹𝐴𝐷 )
7 eqid ( 𝑥𝐷 ↦ ( I ‘ 𝐵 ) ) = ( 𝑥𝐷 ↦ ( I ‘ 𝐵 ) )
8 4 7 fvmptex ( 𝐹𝐴 ) = ( ( 𝑥𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 )
9 fvex ( I ‘ 𝐶 ) ∈ V
10 nfcv 𝑥 I
11 10 2 nffv 𝑥 ( I ‘ 𝐶 )
12 3 fveq2d ( 𝑥 = 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) )
13 1 11 12 7 fvmptf ( ( 𝐴𝐷 ∧ ( I ‘ 𝐶 ) ∈ V ) → ( ( 𝑥𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
14 9 13 mpan2 ( 𝐴𝐷 → ( ( 𝑥𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
15 8 14 eqtrid ( 𝐴𝐷 → ( 𝐹𝐴 ) = ( I ‘ 𝐶 ) )
16 fvprc ( ¬ 𝐶 ∈ V → ( I ‘ 𝐶 ) = ∅ )
17 15 16 sylan9eq ( ( 𝐴𝐷 ∧ ¬ 𝐶 ∈ V ) → ( 𝐹𝐴 ) = ∅ )
18 17 expcom ( ¬ 𝐶 ∈ V → ( 𝐴𝐷 → ( 𝐹𝐴 ) = ∅ ) )
19 6 18 syl5 ( ¬ 𝐶 ∈ V → ( 𝐴 ∈ dom 𝐹 → ( 𝐹𝐴 ) = ∅ ) )
20 ndmfv ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹𝐴 ) = ∅ )
21 19 20 pm2.61d1 ( ¬ 𝐶 ∈ V → ( 𝐹𝐴 ) = ∅ )