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

Metamath Proof Explorer

Theorem fconst7v

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022) Removed hyphotheses as suggested by SN (Revised by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses fconst7v.f ⊢ φ → F Fn A
fconst7v.e ⊢ φ ∧ x ∈ A → F ⁡ x = B
Assertion fconst7v ⊢ φ → F = A × B

Proof

Step Hyp Ref Expression
1 fconst7v.f ⊢ φ → F Fn A
2 fconst7v.e ⊢ φ ∧ x ∈ A → F ⁡ x = B
3 0xp ⊢ ∅ × B = ∅
4 3 a1i ⊢ φ ∧ A = ∅ → ∅ × B = ∅
5 simpr ⊢ φ ∧ A = ∅ → A = ∅
6 5 xpeq1d ⊢ φ ∧ A = ∅ → A × B = ∅ × B
7 1 adantr ⊢ φ ∧ A = ∅ → F Fn A
8 fneq2 ⊢ A = ∅ → F Fn A ↔ F Fn ∅
9 8 adantl ⊢ φ ∧ A = ∅ → F Fn A ↔ F Fn ∅
10 7 9 mpbid ⊢ φ ∧ A = ∅ → F Fn ∅
11 fn0 ⊢ F Fn ∅ ↔ F = ∅
12 10 11 sylib ⊢ φ ∧ A = ∅ → F = ∅
13 4 6 12 3eqtr4rd ⊢ φ ∧ A = ∅ → F = A × B
14 fvexd ⊢ φ ∧ x ∈ A → F ⁡ x ∈ V
15 2 14 eqeltrrd ⊢ φ ∧ x ∈ A → B ∈ V
16 snidg ⊢ B ∈ V → B ∈ B
17 15 16 syl ⊢ φ ∧ x ∈ A → B ∈ B
18 2 17 eqeltrd ⊢ φ ∧ x ∈ A → F ⁡ x ∈ B
19 18 ralrimiva ⊢ φ → ∀ x ∈ A F ⁡ x ∈ B
20 nfcv ⊢ Ⅎ _ x A
21 nfcv ⊢ Ⅎ _ x B
22 nfcv ⊢ Ⅎ _ x F
23 20 21 22 ffnfvf ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
24 1 19 23 sylanbrc ⊢ φ → F : A ⟶ B
25 24 adantr ⊢ φ ∧ A ≠ ∅ → F : A ⟶ B
26 simpr ⊢ φ ∧ A ≠ ∅ → A ≠ ∅
27 15 adantlr ⊢ φ ∧ A ≠ ∅ ∧ x ∈ A → B ∈ V
28 26 27 n0limd ⊢ φ ∧ A ≠ ∅ → B ∈ V
29 fconst2g ⊢ B ∈ V → F : A ⟶ B ↔ F = A × B
30 28 29 syl ⊢ φ ∧ A ≠ ∅ → F : A ⟶ B ↔ F = A × B
31 25 30 mpbid ⊢ φ ∧ A ≠ ∅ → F = A × B
32 exmidne ⊢ A = ∅ ∨ A ≠ ∅
33 32 a1i ⊢ φ → A = ∅ ∨ A ≠ ∅
34 13 31 33 mpjaodan ⊢ φ → F = A × B