lmflf

Description: The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	lmflf.1	$⊢ Z = ℤ_{\geq M}$
	lmflf.2	$⊢ L = Z filGen ℤ_{\geq} [Z]$
Assertion	lmflf	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to (F \underset{t}{⇝} (J) P \leftrightarrow P \in (J fLimf L) (F))$

Proof

Step	Hyp	Ref	Expression
1		lmflf.1	$⊢ Z = ℤ_{\geq M}$
2		lmflf.2	$⊢ L = Z filGen ℤ_{\geq} [Z]$
3		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
4		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
5	3 4	ax-mp	$⊢ ℤ_{\geq} Fn ℤ$
6		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
7	1 6	eqsstri	$⊢ Z \subseteq ℤ$
8		imaeq2	$⊢ y = ℤ_{\geq j} \to F [y] = F [ℤ_{\geq j}]$
9	8	sseq1d	$⊢ y = ℤ_{\geq j} \to (F [y] \subseteq x \leftrightarrow F [ℤ_{\geq j}] \subseteq x)$
10	9	rexima	$⊢ (ℤ_{\geq} Fn ℤ \land Z \subseteq ℤ) \to (\exists y \in ℤ_{\geq} [Z] F [y] \subseteq x \leftrightarrow \exists j \in Z F [ℤ_{\geq j}] \subseteq x)$
11	5 7 10	mp2an	$⊢ \exists y \in ℤ_{\geq} [Z] F [y] \subseteq x \leftrightarrow \exists j \in Z F [ℤ_{\geq j}] \subseteq x$
12		simpl3	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to F : Z ⟶ X$
13	12	ffund	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to Fun F$
14		uzss	$⊢ j \in ℤ_{\geq M} \to ℤ_{\geq j} \subseteq ℤ_{\geq M}$
15	14 1	eleq2s	$⊢ j \in Z \to ℤ_{\geq j} \subseteq ℤ_{\geq M}$
16	15	adantl	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to ℤ_{\geq j} \subseteq ℤ_{\geq M}$
17	12	fdmd	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to dom F = Z$
18	17 1	eqtrdi	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to dom F = ℤ_{\geq M}$
19	16 18	sseqtrrd	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to ℤ_{\geq j} \subseteq dom F$
20		funimass4	$⊢ (Fun F \land ℤ_{\geq j} \subseteq dom F) \to (F [ℤ_{\geq j}] \subseteq x \leftrightarrow \forall k \in ℤ_{\geq j} F (k) \in x)$
21	13 19 20	syl2anc	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to (F [ℤ_{\geq j}] \subseteq x \leftrightarrow \forall k \in ℤ_{\geq j} F (k) \in x)$
22	21	rexbidva	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to (\exists j \in Z F [ℤ_{\geq j}] \subseteq x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in x)$
23	11 22	bitr2id	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in x \leftrightarrow \exists y \in ℤ_{\geq} [Z] F [y] \subseteq x)$
24	23	imbi2d	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to ((P \in x \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in x) \leftrightarrow (P \in x \to \exists y \in ℤ_{\geq} [Z] F [y] \subseteq x))$
25	24	ralbidv	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to (\forall x \in J (P \in x \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in x) \leftrightarrow \forall x \in J (P \in x \to \exists y \in ℤ_{\geq} [Z] F [y] \subseteq x))$
26	25	anbi2d	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to ((P \in X \land \forall x \in J (P \in x \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in x)) \leftrightarrow (P \in X \land \forall x \in J (P \in x \to \exists y \in ℤ_{\geq} [Z] F [y] \subseteq x)))$
27		simp1	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to J \in TopOn (X)$
28		simp2	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to M \in ℤ$
29		simp3	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to F : Z ⟶ X$
30		eqidd	$⊢ ((J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \land k \in Z) \to F (k) = F (k)$
31	27 1 28 29 30	lmbrf	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall x \in J (P \in x \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in x)))$
32	1	uzfbas	$⊢ M \in ℤ \to ℤ_{\geq} [Z] \in fBas (Z)$
33	2	flffbas	$⊢ (J \in TopOn (X) \land ℤ_{\geq} [Z] \in fBas (Z) \land F : Z ⟶ X) \to (P \in (J fLimf L) (F) \leftrightarrow (P \in X \land \forall x \in J (P \in x \to \exists y \in ℤ_{\geq} [Z] F [y] \subseteq x)))$
34	32 33	syl3an2	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to (P \in (J fLimf L) (F) \leftrightarrow (P \in X \land \forall x \in J (P \in x \to \exists y \in ℤ_{\geq} [Z] F [y] \subseteq x)))$
35	26 31 34	3bitr4d	$⊢ (J \in TopOn (X) \land M \in ℤ \land F : Z ⟶ X) \to (F \underset{t}{⇝} (J) P \leftrightarrow P \in (J fLimf L) (F))$

Metamath Proof Explorer

Theorem lmflf

Proof