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

Metamath Proof Explorer

Theorem fconst7

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses fconst7.p ⊢ Ⅎ x φ
fconst7.x ⊢ Ⅎ _ x F
fconst7.f ⊢ φ → F Fn A
fconst7.b ⊢ φ → B ∈ V
fconst7.e ⊢ φ ∧ x ∈ A → F ⁡ x = B
Assertion fconst7 ⊢ φ → F = A × B

Proof

Step Hyp Ref Expression
1 fconst7.p ⊢ Ⅎ x φ
2 fconst7.x ⊢ Ⅎ _ x F
3 fconst7.f ⊢ φ → F Fn A
4 fconst7.b ⊢ φ → B ∈ V
5 fconst7.e ⊢ φ ∧ x ∈ A → F ⁡ x = B
6 fvexd ⊢ φ ∧ x ∈ A → F ⁡ x ∈ V
7 5 6 eqeltrrd ⊢ φ ∧ x ∈ A → B ∈ V
8 snidg ⊢ B ∈ V → B ∈ B
9 7 8 syl ⊢ φ ∧ x ∈ A → B ∈ B
10 5 9 eqeltrd ⊢ φ ∧ x ∈ A → F ⁡ x ∈ B
11 1 10 ralrimia ⊢ φ → ∀ x ∈ A F ⁡ x ∈ B
12 nfcv ⊢ Ⅎ _ x A
13 nfcv ⊢ Ⅎ _ x B
14 12 13 2 ffnfvf ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
15 3 11 14 sylanbrc ⊢ φ → F : A ⟶ B
16 fconst2g ⊢ B ∈ V → F : A ⟶ B ↔ F = A × B
17 4 16 syl ⊢ φ → F : A ⟶ B ↔ F = A × B
18 15 17 mpbid ⊢ φ → F = A × B