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

Metamath Proof Explorer

Theorem fvmptex

Description: Express a function F whose value B may not always be a set in terms of another function G for which sethood is guaranteed. (Note that (IB ) is just shorthand for if ( B e. V , B , (/) ) , and it is always a set by fvex .) Note also that these functions are not the same; wherever B ( C ) is not a set, C is not in the domain of F (so it evaluates to the empty set), but C is in the domain of G , and G ( C ) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fvmptex.1 ⊢ F = x ∈ A ⟼ B
fvmptex.2 ⊢ G = x ∈ A ⟼ I ⁡ B
Assertion fvmptex ⊢ F ⁡ C = G ⁡ C

Proof

Step Hyp Ref Expression
1 fvmptex.1 ⊢ F = x ∈ A ⟼ B
2 fvmptex.2 ⊢ G = x ∈ A ⟼ I ⁡ B
3 csbeq1 ⊢ y = C → ⦋ y / x⦌ B = ⦋ C / x⦌ B
4 nfcv ⊢ Ⅎ _ y B
5 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
6 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
7 4 5 6 cbvmpt ⊢ x ∈ A ⟼ B = y ∈ A ⟼ ⦋ y / x⦌ B
8 1 7 eqtri ⊢ F = y ∈ A ⟼ ⦋ y / x⦌ B
9 3 8 fvmpti ⊢ C ∈ A → F ⁡ C = I ⁡ ⦋ C / x⦌ B
10 3 fveq2d ⊢ y = C → I ⁡ ⦋ y / x⦌ B = I ⁡ ⦋ C / x⦌ B
11 nfcv ⊢ Ⅎ _ y I ⁡ B
12 nfcv ⊢ Ⅎ _ x I
13 12 5 nffv ⊢ Ⅎ _ x I ⁡ ⦋ y / x⦌ B
14 6 fveq2d ⊢ x = y → I ⁡ B = I ⁡ ⦋ y / x⦌ B
15 11 13 14 cbvmpt ⊢ x ∈ A ⟼ I ⁡ B = y ∈ A ⟼ I ⁡ ⦋ y / x⦌ B
16 2 15 eqtri ⊢ G = y ∈ A ⟼ I ⁡ ⦋ y / x⦌ B
17 fvex ⊢ I ⁡ ⦋ C / x⦌ B ∈ V
18 10 16 17 fvmpt ⊢ C ∈ A → G ⁡ C = I ⁡ ⦋ C / x⦌ B
19 9 18 eqtr4d ⊢ C ∈ A → F ⁡ C = G ⁡ C
20 1 dmmptss ⊢ dom ⁡ F ⊆ A
21 20 sseli ⊢ C ∈ dom ⁡ F → C ∈ A
22 ndmfv ⊢ ¬ C ∈ dom ⁡ F → F ⁡ C = ∅
23 21 22 nsyl5 ⊢ ¬ C ∈ A → F ⁡ C = ∅
24 fvex ⊢ I ⁡ B ∈ V
25 24 2 dmmpti ⊢ dom ⁡ G = A
26 25 eleq2i ⊢ C ∈ dom ⁡ G ↔ C ∈ A
27 ndmfv ⊢ ¬ C ∈ dom ⁡ G → G ⁡ C = ∅
28 26 27 sylnbir ⊢ ¬ C ∈ A → G ⁡ C = ∅
29 23 28 eqtr4d ⊢ ¬ C ∈ A → F ⁡ C = G ⁡ C
30 19 29 pm2.61i ⊢ F ⁡ C = G ⁡ C