mpteleeOLD

Description: Obsolete version of mptelee as of 2-Feb-2026. (Contributed by Scott Fenton, 7-Jun-2013) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	mpteleeOLD	$⊢ N \in ℕ \to ((k \in (1 \dots N) ⟼ A F B) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) A F B \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		elee	$⊢ N \in ℕ \to ((k \in (1 \dots N) ⟼ A F B) \in 𝔼 (N) \leftrightarrow (k \in (1 \dots N) ⟼ A F B) : (1 \dots N) ⟶ ℝ)$
2		ovex	$⊢ A F B \in V$
3		eqid	$⊢ (k \in (1 \dots N) ⟼ A F B) = (k \in (1 \dots N) ⟼ A F B)$
4	2 3	fnmpti	$⊢ (k \in (1 \dots N) ⟼ A F B) Fn (1 \dots N)$
5		df-f	$⊢ (k \in (1 \dots N) ⟼ A F B) : (1 \dots N) ⟶ ℝ \leftrightarrow ((k \in (1 \dots N) ⟼ A F B) Fn (1 \dots N) \land ran (k \in (1 \dots N) ⟼ A F B) \subseteq ℝ)$
6	4 5	mpbiran	$⊢ (k \in (1 \dots N) ⟼ A F B) : (1 \dots N) ⟶ ℝ \leftrightarrow ran (k \in (1 \dots N) ⟼ A F B) \subseteq ℝ$
7	3	rnmpt	$⊢ ran (k \in (1 \dots N) ⟼ A F B) = \{a \| \exists k \in (1 \dots N) a = A F B\}$
8	7	sseq1i	$⊢ ran (k \in (1 \dots N) ⟼ A F B) \subseteq ℝ \leftrightarrow \{a \| \exists k \in (1 \dots N) a = A F B\} \subseteq ℝ$
9		abss	$⊢ \{a \| \exists k \in (1 \dots N) a = A F B\} \subseteq ℝ \leftrightarrow \forall a (\exists k \in (1 \dots N) a = A F B \to a \in ℝ)$
10		nfre1	$⊢ Ⅎ k \exists k \in (1 \dots N) a = A F B$
11		nfv	$⊢ Ⅎ k a \in ℝ$
12	10 11	nfim	$⊢ Ⅎ k (\exists k \in (1 \dots N) a = A F B \to a \in ℝ)$
13	12	nfal	$⊢ Ⅎ k \forall a (\exists k \in (1 \dots N) a = A F B \to a \in ℝ)$
14		r19.23v	$⊢ \forall k \in (1 \dots N) (a = A F B \to a \in ℝ) \leftrightarrow (\exists k \in (1 \dots N) a = A F B \to a \in ℝ)$
15	14	albii	$⊢ \forall a \forall k \in (1 \dots N) (a = A F B \to a \in ℝ) \leftrightarrow \forall a (\exists k \in (1 \dots N) a = A F B \to a \in ℝ)$
16		ralcom4	$⊢ \forall k \in (1 \dots N) \forall a (a = A F B \to a \in ℝ) \leftrightarrow \forall a \forall k \in (1 \dots N) (a = A F B \to a \in ℝ)$
17		rsp	$⊢ \forall k \in (1 \dots N) \forall a (a = A F B \to a \in ℝ) \to (k \in (1 \dots N) \to \forall a (a = A F B \to a \in ℝ))$
18	2	clel2	$⊢ A F B \in ℝ \leftrightarrow \forall a (a = A F B \to a \in ℝ)$
19	17 18	imbitrrdi	$⊢ \forall k \in (1 \dots N) \forall a (a = A F B \to a \in ℝ) \to (k \in (1 \dots N) \to A F B \in ℝ)$
20	16 19	sylbir	$⊢ \forall a \forall k \in (1 \dots N) (a = A F B \to a \in ℝ) \to (k \in (1 \dots N) \to A F B \in ℝ)$
21	15 20	sylbir	$⊢ \forall a (\exists k \in (1 \dots N) a = A F B \to a \in ℝ) \to (k \in (1 \dots N) \to A F B \in ℝ)$
22	13 21	ralrimi	$⊢ \forall a (\exists k \in (1 \dots N) a = A F B \to a \in ℝ) \to \forall k \in (1 \dots N) A F B \in ℝ$
23		nfra1	$⊢ Ⅎ k \forall k \in (1 \dots N) A F B \in ℝ$
24		rsp	$⊢ \forall k \in (1 \dots N) A F B \in ℝ \to (k \in (1 \dots N) \to A F B \in ℝ)$
25		eleq1a	$⊢ A F B \in ℝ \to (a = A F B \to a \in ℝ)$
26	24 25	syl6	$⊢ \forall k \in (1 \dots N) A F B \in ℝ \to (k \in (1 \dots N) \to (a = A F B \to a \in ℝ))$
27	23 11 26	rexlimd	$⊢ \forall k \in (1 \dots N) A F B \in ℝ \to (\exists k \in (1 \dots N) a = A F B \to a \in ℝ)$
28	27	alrimiv	$⊢ \forall k \in (1 \dots N) A F B \in ℝ \to \forall a (\exists k \in (1 \dots N) a = A F B \to a \in ℝ)$
29	22 28	impbii	$⊢ \forall a (\exists k \in (1 \dots N) a = A F B \to a \in ℝ) \leftrightarrow \forall k \in (1 \dots N) A F B \in ℝ$
30	9 29	bitri	$⊢ \{a \| \exists k \in (1 \dots N) a = A F B\} \subseteq ℝ \leftrightarrow \forall k \in (1 \dots N) A F B \in ℝ$
31	8 30	bitri	$⊢ ran (k \in (1 \dots N) ⟼ A F B) \subseteq ℝ \leftrightarrow \forall k \in (1 \dots N) A F B \in ℝ$
32	6 31	bitri	$⊢ (k \in (1 \dots N) ⟼ A F B) : (1 \dots N) ⟶ ℝ \leftrightarrow \forall k \in (1 \dots N) A F B \in ℝ$
33	1 32	bitrdi	$⊢ N \in ℕ \to ((k \in (1 \dots N) ⟼ A F B) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) A F B \in ℝ)$

Metamath Proof Explorer

Theorem mpteleeOLD

Proof