lmss

Description: Limit on a subspace. (Contributed by NM, 30-Jan-2008) (Revised by Mario Carneiro, 30-Dec-2013)

	Ref	Expression
Hypotheses	lmss.1	$⊢ K = J ↾_{𝑡} Y$
	lmss.2	$⊢ Z = ℤ_{\geq M}$
	lmss.3	$⊢ φ \to Y \in V$
	lmss.4	$⊢ φ \to J \in Top$
	lmss.5	$⊢ φ \to P \in Y$
	lmss.6	$⊢ φ \to M \in ℤ$
	lmss.7	$⊢ φ \to F : Z ⟶ Y$
Assertion	lmss	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow F \underset{t}{⇝} (K) P)$

Proof

Step	Hyp	Ref	Expression
1		lmss.1	$⊢ K = J ↾_{𝑡} Y$
2		lmss.2	$⊢ Z = ℤ_{\geq M}$
3		lmss.3	$⊢ φ \to Y \in V$
4		lmss.4	$⊢ φ \to J \in Top$
5		lmss.5	$⊢ φ \to P \in Y$
6		lmss.6	$⊢ φ \to M \in ℤ$
7		lmss.7	$⊢ φ \to F : Z ⟶ Y$
8		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
9	4 8	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
10		lmcl	$⊢ (J \in TopOn (⋃ J) \land F \underset{t}{⇝} (J) P) \to P \in ⋃ J$
11	9 10	sylan	$⊢ (φ \land F \underset{t}{⇝} (J) P) \to P \in ⋃ J$
12		lmfss	$⊢ (J \in TopOn (⋃ J) \land F \underset{t}{⇝} (J) P) \to F \subseteq ℂ \times ⋃ J$
13	9 12	sylan	$⊢ (φ \land F \underset{t}{⇝} (J) P) \to F \subseteq ℂ \times ⋃ J$
14		rnss	$⊢ F \subseteq ℂ \times ⋃ J \to ran F \subseteq ran (ℂ \times ⋃ J)$
15	13 14	syl	$⊢ (φ \land F \underset{t}{⇝} (J) P) \to ran F \subseteq ran (ℂ \times ⋃ J)$
16		rnxpss	$⊢ ran (ℂ \times ⋃ J) \subseteq ⋃ J$
17	15 16	sstrdi	$⊢ (φ \land F \underset{t}{⇝} (J) P) \to ran F \subseteq ⋃ J$
18	11 17	jca	$⊢ (φ \land F \underset{t}{⇝} (J) P) \to (P \in ⋃ J \land ran F \subseteq ⋃ J)$
19	18	ex	$⊢ φ \to (F \underset{t}{⇝} (J) P \to (P \in ⋃ J \land ran F \subseteq ⋃ J))$
20		resttopon2	$⊢ (J \in TopOn (⋃ J) \land Y \in V) \to J ↾_{𝑡} Y \in TopOn (Y \cap ⋃ J)$
21	9 3 20	syl2anc	$⊢ φ \to J ↾_{𝑡} Y \in TopOn (Y \cap ⋃ J)$
22	1 21	eqeltrid	$⊢ φ \to K \in TopOn (Y \cap ⋃ J)$
23		lmcl	$⊢ (K \in TopOn (Y \cap ⋃ J) \land F \underset{t}{⇝} (K) P) \to P \in (Y \cap ⋃ J)$
24	22 23	sylan	$⊢ (φ \land F \underset{t}{⇝} (K) P) \to P \in (Y \cap ⋃ J)$
25	24	elin2d	$⊢ (φ \land F \underset{t}{⇝} (K) P) \to P \in ⋃ J$
26		lmfss	$⊢ (K \in TopOn (Y \cap ⋃ J) \land F \underset{t}{⇝} (K) P) \to F \subseteq ℂ \times (Y \cap ⋃ J)$
27	22 26	sylan	$⊢ (φ \land F \underset{t}{⇝} (K) P) \to F \subseteq ℂ \times (Y \cap ⋃ J)$
28		rnss	$⊢ F \subseteq ℂ \times (Y \cap ⋃ J) \to ran F \subseteq ran (ℂ \times (Y \cap ⋃ J))$
29	27 28	syl	$⊢ (φ \land F \underset{t}{⇝} (K) P) \to ran F \subseteq ran (ℂ \times (Y \cap ⋃ J))$
30		rnxpss	$⊢ ran (ℂ \times (Y \cap ⋃ J)) \subseteq Y \cap ⋃ J$
31	29 30	sstrdi	$⊢ (φ \land F \underset{t}{⇝} (K) P) \to ran F \subseteq Y \cap ⋃ J$
32		inss2	$⊢ Y \cap ⋃ J \subseteq ⋃ J$
33	31 32	sstrdi	$⊢ (φ \land F \underset{t}{⇝} (K) P) \to ran F \subseteq ⋃ J$
34	25 33	jca	$⊢ (φ \land F \underset{t}{⇝} (K) P) \to (P \in ⋃ J \land ran F \subseteq ⋃ J)$
35	34	ex	$⊢ φ \to (F \underset{t}{⇝} (K) P \to (P \in ⋃ J \land ran F \subseteq ⋃ J))$
36		simprl	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to P \in ⋃ J$
37	5	adantr	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to P \in Y$
38	37 36	elind	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to P \in (Y \cap ⋃ J)$
39	36 38	2thd	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (P \in ⋃ J \leftrightarrow P \in (Y \cap ⋃ J))$
40	1	eleq2i	$⊢ v \in K \leftrightarrow v \in (J ↾_{𝑡} Y)$
41	4	adantr	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to J \in Top$
42	3	adantr	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to Y \in V$
43		elrest	$⊢ (J \in Top \land Y \in V) \to (v \in (J ↾_{𝑡} Y) \leftrightarrow \exists u \in J v = u \cap Y)$
44	41 42 43	syl2anc	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (v \in (J ↾_{𝑡} Y) \leftrightarrow \exists u \in J v = u \cap Y)$
45	44	biimpa	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land v \in (J ↾_{𝑡} Y)) \to \exists u \in J v = u \cap Y$
46	40 45	sylan2b	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land v \in K) \to \exists u \in J v = u \cap Y$
47		r19.29r	$⊢ (\exists u \in J v = u \cap Y \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)) \to \exists u \in J (v = u \cap Y \land (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
48	37	biantrud	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (P \in u \leftrightarrow (P \in u \land P \in Y))$
49		elin	$⊢ P \in (u \cap Y) \leftrightarrow (P \in u \land P \in Y)$
50	48 49	bitr4di	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (P \in u \leftrightarrow P \in (u \cap Y))$
51	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
52	7	adantr	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to F : Z ⟶ Y$
53	52	ffvelcdmda	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land k \in Z) \to F (k) \in Y$
54	53	biantrud	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land k \in Z) \to (F (k) \in u \leftrightarrow (F (k) \in u \land F (k) \in Y))$
55		elin	$⊢ F (k) \in (u \cap Y) \leftrightarrow (F (k) \in u \land F (k) \in Y)$
56	54 55	bitr4di	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land k \in Z) \to (F (k) \in u \leftrightarrow F (k) \in (u \cap Y))$
57	51 56	sylan2	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land (j \in Z \land k \in ℤ_{\geq j})) \to (F (k) \in u \leftrightarrow F (k) \in (u \cap Y))$
58	57	anassrs	$⊢ (((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (k) \in u \leftrightarrow F (k) \in (u \cap Y))$
59	58	ralbidva	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land j \in Z) \to (\forall k \in ℤ_{\geq j} F (k) \in u \leftrightarrow \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y))$
60	59	rexbidva	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y))$
61	50 60	imbi12d	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \leftrightarrow (P \in (u \cap Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y)))$
62	61	adantr	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \leftrightarrow (P \in (u \cap Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y)))$
63	62	biimpd	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to (P \in (u \cap Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y)))$
64		eleq2	$⊢ v = u \cap Y \to (P \in v \leftrightarrow P \in (u \cap Y))$
65		eleq2	$⊢ v = u \cap Y \to (F (k) \in v \leftrightarrow F (k) \in (u \cap Y))$
66	65	rexralbidv	$⊢ v = u \cap Y \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y))$
67	64 66	imbi12d	$⊢ v = u \cap Y \to ((P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v) \leftrightarrow (P \in (u \cap Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y)))$
68	67	imbi2d	$⊢ v = u \cap Y \to (((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v)) \leftrightarrow ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to (P \in (u \cap Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y))))$
69	63 68	syl5ibrcom	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to (v = u \cap Y \to ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v)))$
70	69	impd	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to ((v = u \cap Y \land (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)) \to (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v))$
71	70	rexlimdva	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (\exists u \in J (v = u \cap Y \land (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)) \to (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v))$
72	47 71	syl5	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to ((\exists u \in J v = u \cap Y \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)) \to (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v))$
73	72	expdimp	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land \exists u \in J v = u \cap Y) \to (\forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v))$
74	46 73	syldan	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land v \in K) \to (\forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v))$
75	74	ralrimdva	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (\forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to \forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v))$
76	41	adantr	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to J \in Top$
77	42	adantr	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to Y \in V$
78		simpr	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to u \in J$
79		elrestr	$⊢ (J \in Top \land Y \in V \land u \in J) \to u \cap Y \in (J ↾_{𝑡} Y)$
80	76 77 78 79	syl3anc	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to u \cap Y \in (J ↾_{𝑡} Y)$
81	80 1	eleqtrrdi	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to u \cap Y \in K$
82	67	rspcv	$⊢ u \cap Y \in K \to (\forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v) \to (P \in (u \cap Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y)))$
83	81 82	syl	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to (\forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v) \to (P \in (u \cap Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (u \cap Y)))$
84	83 62	sylibrd	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land u \in J) \to (\forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v) \to (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
85	84	ralrimdva	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (\forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v) \to \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
86	75 85	impbid	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (\forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \leftrightarrow \forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v))$
87	39 86	anbi12d	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to ((P \in ⋃ J \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)) \leftrightarrow (P \in (Y \cap ⋃ J) \land \forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v)))$
88	41 8	sylib	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to J \in TopOn (⋃ J)$
89	6	adantr	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to M \in ℤ$
90	52	ffnd	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to F Fn Z$
91		simprr	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to ran F \subseteq ⋃ J$
92		df-f	$⊢ F : Z ⟶ ⋃ J \leftrightarrow (F Fn Z \land ran F \subseteq ⋃ J)$
93	90 91 92	sylanbrc	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to F : Z ⟶ ⋃ J$
94		eqidd	$⊢ ((φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \land k \in Z) \to F (k) = F (k)$
95	88 2 89 93 94	lmbrf	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in ⋃ J \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)))$
96	22	adantr	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to K \in TopOn (Y \cap ⋃ J)$
97	52	frnd	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to ran F \subseteq Y$
98	97 91	ssind	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to ran F \subseteq Y \cap ⋃ J$
99		df-f	$⊢ F : Z ⟶ Y \cap ⋃ J \leftrightarrow (F Fn Z \land ran F \subseteq Y \cap ⋃ J)$
100	90 98 99	sylanbrc	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to F : Z ⟶ Y \cap ⋃ J$
101	96 2 89 100 94	lmbrf	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (F \underset{t}{⇝} (K) P \leftrightarrow (P \in (Y \cap ⋃ J) \land \forall v \in K (P \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in v)))$
102	87 95 101	3bitr4d	$⊢ (φ \land (P \in ⋃ J \land ran F \subseteq ⋃ J)) \to (F \underset{t}{⇝} (J) P \leftrightarrow F \underset{t}{⇝} (K) P)$
103	102	ex	$⊢ φ \to ((P \in ⋃ J \land ran F \subseteq ⋃ J) \to (F \underset{t}{⇝} (J) P \leftrightarrow F \underset{t}{⇝} (K) P))$
104	19 35 103	pm5.21ndd	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow F \underset{t}{⇝} (K) P)$

Metamath Proof Explorer

Theorem lmss

Proof