cnpflfi

		Ref	Expression
	Assertion	cnpflfi	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to F (A) \in (K fLimf L) (F)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2		eqid	$⊢ ⋃ K = ⋃ K$
3	1 2	cnpf	$⊢ F \in (J CnP K) (A) \to F : ⋃ J ⟶ ⋃ K$
4	3	adantl	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to F : ⋃ J ⟶ ⋃ K$
5	1	flimelbas	$⊢ A \in (J fLim L) \to A \in ⋃ J$
6	5	adantr	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to A \in ⋃ J$
7	4 6	ffvelcdmd	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to F (A) \in ⋃ K$
8		simplr	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to F \in (J CnP K) (A)$
9		simprl	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to x \in K$
10		simprr	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to F (A) \in x$
11		cnpimaex	$⊢ (F \in (J CnP K) (A) \land x \in K \land F (A) \in x) \to \exists y \in J (A \in y \land F [y] \subseteq x)$
12	8 9 10 11	syl3anc	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to \exists y \in J (A \in y \land F [y] \subseteq x)$
13		anass	$⊢ ((y \in J \land A \in y) \land F [y] \subseteq x) \leftrightarrow (y \in J \land (A \in y \land F [y] \subseteq x))$
14		simpl	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to A \in (J fLim L)$
15		flimtop	$⊢ A \in (J fLim L) \to J \in Top$
16	15	adantr	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to J \in Top$
17		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
18	16 17	sylib	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to J \in TopOn (⋃ J)$
19	1	flimfil	$⊢ A \in (J fLim L) \to L \in Fil (⋃ J)$
20	19	adantr	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to L \in Fil (⋃ J)$
21		flimopn	$⊢ (J \in TopOn (⋃ J) \land L \in Fil (⋃ J)) \to (A \in (J fLim L) \leftrightarrow (A \in ⋃ J \land \forall y \in J (A \in y \to y \in L)))$
22	18 20 21	syl2anc	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to (A \in (J fLim L) \leftrightarrow (A \in ⋃ J \land \forall y \in J (A \in y \to y \in L)))$
23	14 22	mpbid	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to (A \in ⋃ J \land \forall y \in J (A \in y \to y \in L))$
24	23	simprd	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to \forall y \in J (A \in y \to y \in L)$
25	24	adantr	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to \forall y \in J (A \in y \to y \in L)$
26	25	r19.21bi	$⊢ (((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \land y \in J) \to (A \in y \to y \in L)$
27	26	expimpd	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to ((y \in J \land A \in y) \to y \in L)$
28	27	anim1d	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to (((y \in J \land A \in y) \land F [y] \subseteq x) \to (y \in L \land F [y] \subseteq x))$
29	13 28	biimtrrid	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to ((y \in J \land (A \in y \land F [y] \subseteq x)) \to (y \in L \land F [y] \subseteq x))$
30	29	reximdv2	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to (\exists y \in J (A \in y \land F [y] \subseteq x) \to \exists y \in L F [y] \subseteq x)$
31	12 30	mpd	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land (x \in K \land F (A) \in x)) \to \exists y \in L F [y] \subseteq x$
32	31	expr	$⊢ ((A \in (J fLim L) \land F \in (J CnP K) (A)) \land x \in K) \to (F (A) \in x \to \exists y \in L F [y] \subseteq x)$
33	32	ralrimiva	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to \forall x \in K (F (A) \in x \to \exists y \in L F [y] \subseteq x)$
34		cnptop2	$⊢ F \in (J CnP K) (A) \to K \in Top$
35	34	adantl	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to K \in Top$
36		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
37	35 36	sylib	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to K \in TopOn (⋃ K)$
38		isflf	$⊢ (K \in TopOn (⋃ K) \land L \in Fil (⋃ J) \land F : ⋃ J ⟶ ⋃ K) \to (F (A) \in (K fLimf L) (F) \leftrightarrow (F (A) \in ⋃ K \land \forall x \in K (F (A) \in x \to \exists y \in L F [y] \subseteq x)))$
39	37 20 4 38	syl3anc	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to (F (A) \in (K fLimf L) (F) \leftrightarrow (F (A) \in ⋃ K \land \forall x \in K (F (A) \in x \to \exists y \in L F [y] \subseteq x)))$
40	7 33 39	mpbir2and	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to F (A) \in (K fLimf L) (F)$

Metamath Proof Explorer

Theorem cnpflfi

Proof