mbfmullem

	Ref	Expression
Hypotheses	mbfmul.1	$⊢ φ \to F \in MblFn$
	mbfmul.2	$⊢ φ \to G \in MblFn$
	mbfmul.3	$⊢ φ \to F : A ⟶ ℝ$
	mbfmul.4	$⊢ φ \to G : A ⟶ ℝ$
Assertion	mbfmullem	$⊢ φ \to F \times_{f} G \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfmul.1	$⊢ φ \to F \in MblFn$
2		mbfmul.2	$⊢ φ \to G \in MblFn$
3		mbfmul.3	$⊢ φ \to F : A ⟶ ℝ$
4		mbfmul.4	$⊢ φ \to G : A ⟶ ℝ$
5	1 3	mbfi1flim	$⊢ φ \to \exists f (f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y))$
6	2 4	mbfi1flim	$⊢ φ \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y))$
7		exdistrv	$⊢ \exists f \exists g ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y))) \leftrightarrow (\exists f (f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land \exists g (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))$
8	1	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to F \in MblFn$
9	2	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to G \in MblFn$
10	3	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to F : A ⟶ ℝ$
11	4	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to G : A ⟶ ℝ$
12		simprll	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to f : ℕ ⟶ dom \int^{1}$
13		simprlr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)$
14		fveq2	$⊢ y = x \to f (n) (y) = f (n) (x)$
15	14	mpteq2dv	$⊢ y = x \to (n \in ℕ ⟼ f (n) (y)) = (n \in ℕ ⟼ f (n) (x))$
16		fveq2	$⊢ n = m \to f (n) = f (m)$
17	16	fveq1d	$⊢ n = m \to f (n) (x) = f (m) (x)$
18	17	cbvmptv	$⊢ (n \in ℕ ⟼ f (n) (x)) = (m \in ℕ ⟼ f (m) (x))$
19	15 18	eqtrdi	$⊢ y = x \to (n \in ℕ ⟼ f (n) (y)) = (m \in ℕ ⟼ f (m) (x))$
20		fveq2	$⊢ y = x \to F (y) = F (x)$
21	19 20	breq12d	$⊢ y = x \to ((n \in ℕ ⟼ f (n) (y)) ⇝ F (y) \leftrightarrow (m \in ℕ ⟼ f (m) (x)) ⇝ F (x))$
22	21	rspccva	$⊢ (\forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y) \land x \in A) \to (m \in ℕ ⟼ f (m) (x)) ⇝ F (x)$
23	13 22	sylan	$⊢ ((φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \land x \in A) \to (m \in ℕ ⟼ f (m) (x)) ⇝ F (x)$
24		simprrl	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to g : ℕ ⟶ dom \int^{1}$
25		simprrr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)$
26		fveq2	$⊢ y = x \to g (n) (y) = g (n) (x)$
27	26	mpteq2dv	$⊢ y = x \to (n \in ℕ ⟼ g (n) (y)) = (n \in ℕ ⟼ g (n) (x))$
28		fveq2	$⊢ n = m \to g (n) = g (m)$
29	28	fveq1d	$⊢ n = m \to g (n) (x) = g (m) (x)$
30	29	cbvmptv	$⊢ (n \in ℕ ⟼ g (n) (x)) = (m \in ℕ ⟼ g (m) (x))$
31	27 30	eqtrdi	$⊢ y = x \to (n \in ℕ ⟼ g (n) (y)) = (m \in ℕ ⟼ g (m) (x))$
32		fveq2	$⊢ y = x \to G (y) = G (x)$
33	31 32	breq12d	$⊢ y = x \to ((n \in ℕ ⟼ g (n) (y)) ⇝ G (y) \leftrightarrow (m \in ℕ ⟼ g (m) (x)) ⇝ G (x))$
34	33	rspccva	$⊢ (\forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y) \land x \in A) \to (m \in ℕ ⟼ g (m) (x)) ⇝ G (x)$
35	25 34	sylan	$⊢ ((φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \land x \in A) \to (m \in ℕ ⟼ g (m) (x)) ⇝ G (x)$
36	8 9 10 11 12 23 24 35	mbfmullem2	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y)))) \to F \times_{f} G \in MblFn$
37	36	ex	$⊢ φ \to (((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y))) \to F \times_{f} G \in MblFn)$
38	37	exlimdvv	$⊢ φ \to (\exists f \exists g ((f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y))) \to F \times_{f} G \in MblFn)$
39	7 38	syl5bir	$⊢ φ \to ((\exists f (f : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ f (n) (y)) ⇝ F (y)) \land \exists g (g : ℕ ⟶ dom \int^{1} \land \forall y \in A (n \in ℕ ⟼ g (n) (y)) ⇝ G (y))) \to F \times_{f} G \in MblFn)$
40	5 6 39	mp2and	$⊢ φ \to F \times_{f} G \in MblFn$

Metamath Proof Explorer

Theorem mbfmullem

Proof