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 ⊢ Ⅎ 𝑥 𝐴
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 → ( 𝐹 ‘ 𝐴 ) = ∅ )