txlly

Description: If the property A is preserved under topological products, then so is the property of being locally A . (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Hypothesis	txlly.1	$⊢ (j \in A \land k \in A) \to j \times_{t} k \in A$
	Assertion	txlly	$⊢ (R \in LocallyA\landS \in LocallyA\toR \times_{t} S \in LocallyA)$

Proof

Step	Hyp	Ref	Expression
1		txlly.1	$⊢ (j \in A \land k \in A) \to j \times_{t} k \in A$
2		llytop	$⊢ R \in LocallyA\toR \in Top$
3		llytop	$⊢ S \in LocallyA\toS \in Top$
4		txtop	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$
5	2 3 4	syl2an	$⊢ (R \in LocallyA\landS \in LocallyA\toR \times_{t} S \in Top)$
6		eltx	$⊢ (R \in LocallyA\landS \in LocallyA\to(x \in (R \times_{t} S) \leftrightarrow \forall y \in x \exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq x)))$
7		simpll	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toR \in LocallyA))$
8		simprll	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\tou \in R))$
9		simprrl	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toy \in (u \times v)))$
10		xp1st	$⊢ y \in (u \times v) \to 1^{st} (y) \in u$
11	9 10	syl	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to1^{st} (y) \in u))$
12		llyi	$⊢ (R \in LocallyA\landu \in R\land1^{st} (y) \in u\to\exists r \in R (r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A))$
13	7 8 11 12	syl3anc	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to\exists r \in R (r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A)))$
14		simplr	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toS \in LocallyA))$
15		simprlr	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\tov \in S))$
16		xp2nd	$⊢ y \in (u \times v) \to 2^{nd} (y) \in v$
17	9 16	syl	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to2^{nd} (y) \in v))$
18		llyi	$⊢ (S \in LocallyA\landv \in S\land2^{nd} (y) \in v\to\exists s \in S (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))$
19	14 15 17 18	syl3anc	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to\exists s \in S (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))$
20		reeanv	$⊢ \exists r \in R \exists s \in S ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)) \leftrightarrow (\exists r \in R (r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land \exists s \in S (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))$
21	2	ad3antrrr	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\toR \in Top)))$
22	3	ad3antlr	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\toS \in Top)))$
23		simprll	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\tor \in R)))$
24		simprlr	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\tos \in S)))$
25		txopn	$⊢ ((R \in Top \land S \in Top) \land (r \in R \land s \in S)) \to r \times s \in (R \times_{t} S)$
26	21 22 23 24 25	syl22anc	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\tor \times s \in (R \times_{t} S))))$
27		simprl1	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to r \subseteq u$
28		simprr1	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to s \subseteq v$
29		xpss12	$⊢ (r \subseteq u \land s \subseteq v) \to r \times s \subseteq u \times v$
30	27 28 29	syl2anc	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to r \times s \subseteq u \times v$
31		simprrr	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\tou \times v \subseteq x))$
32	30 31	sylan9ssr	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\tor \times s \subseteq x)))$
33		vex	$⊢ x \in V$
34	33	elpw2	$⊢ r \times s \in 𝒫 x \leftrightarrow r \times s \subseteq x$
35	32 34	sylibr	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\tor \times s \in 𝒫 x)))$
36	26 35	elind	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\tor \times s \in ((R \times_{t} S) \cap 𝒫 x))))$
37		1st2nd2	$⊢ y \in (u \times v) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
38	9 37	syl	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toy = ⟨1^{st} (y), 2^{nd} (y)⟩))$
39	38	adantr	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\toy = ⟨1^{st} (y), 2^{nd} (y)⟩)))$
40		simprl2	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to 1^{st} (y) \in r$
41		simprr2	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to 2^{nd} (y) \in s$
42	40 41	opelxpd	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to ⟨1^{st} (y), 2^{nd} (y)⟩ \in (r \times s)$
43	42	adantl	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\to⟨1^{st} (y), 2^{nd} (y)⟩ \in (r \times s))))$
44	39 43	eqeltrd	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\toy \in (r \times s))))$
45		txrest	$⊢ ((R \in Top \land S \in Top) \land (r \in R \land s \in S)) \to (R \times_{t} S) ↾_{𝑡} (r \times s) = (R ↾_{𝑡} r) \times_{t} (S ↾_{𝑡} s)$
46	21 22 23 24 45	syl22anc	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\to(R \times_{t} S) ↾_{𝑡} (r \times s) = (R ↾_{𝑡} r) \times_{t} (S ↾_{𝑡} s))))$
47		simprl3	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to R ↾_{𝑡} r \in A$
48		simprr3	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to S ↾_{𝑡} s \in A$
49	1	caovcl	$⊢ (R ↾_{𝑡} r \in A \land S ↾_{𝑡} s \in A) \to (R ↾_{𝑡} r) \times_{t} (S ↾_{𝑡} s) \in A$
50	47 48 49	syl2anc	$⊢ ((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A))) \to (R ↾_{𝑡} r) \times_{t} (S ↾_{𝑡} s) \in A$
51	50	adantl	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\to(R ↾_{𝑡} r) \times_{t} (S ↾_{𝑡} s) \in A)))$
52	46 51	eqeltrd	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\to(R \times_{t} S) ↾_{𝑡} (r \times s) \in A)))$
53		eleq2	$⊢ z = r \times s \to (y \in z \leftrightarrow y \in (r \times s))$
54		oveq2	$⊢ z = r \times s \to (R \times_{t} S) ↾_{𝑡} z = (R \times_{t} S) ↾_{𝑡} (r \times s)$
55	54	eleq1d	$⊢ z = r \times s \to ((R \times_{t} S) ↾_{𝑡} z \in A \leftrightarrow (R \times_{t} S) ↾_{𝑡} (r \times s) \in A)$
56	53 55	anbi12d	$⊢ z = r \times s \to ((y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A) \leftrightarrow (y \in (r \times s) \land (R \times_{t} S) ↾_{𝑡} (r \times s) \in A))$
57	56	rspcev	$⊢ (r \times s \in ((R \times_{t} S) \cap 𝒫 x) \land (y \in (r \times s) \land (R \times_{t} S) ↾_{𝑡} (r \times s) \in A)) \to \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A)$
58	36 44 52 57	syl12anc	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((r \in R \land s \in S) \land ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)))\to\exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A))))$
59	58	expr	$⊢ (((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land(r \in R \land s \in S)\to(((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)) \to \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A)))))$
60	59	rexlimdvva	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to(\exists r \in R \exists s \in S ((r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)) \to \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A))))$
61	20 60	biimtrrid	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to((\exists r \in R (r \subseteq u \land 1^{st} (y) \in r \land R ↾_{𝑡} r \in A) \land \exists s \in S (s \subseteq v \land 2^{nd} (y) \in s \land S ↾_{𝑡} s \in A)) \to \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A))))$
62	13 19 61	mp2and	$⊢ ((R \in LocallyA\landS \in LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to\exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A)))$
63	62	expr	$⊢ ((R \in LocallyA\landS \in LocallyA\land(u \in R \land v \in S)\to((y \in (u \times v) \land u \times v \subseteq x) \to \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A))))$
64	63	rexlimdvva	$⊢ (R \in LocallyA\landS \in LocallyA\to(\exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq x) \to \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A)))$
65	64	ralimdv	$⊢ (R \in LocallyA\landS \in LocallyA\to(\forall y \in x \exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq x) \to \forall y \in x \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A)))$
66	6 65	sylbid	$⊢ (R \in LocallyA\landS \in LocallyA\to(x \in (R \times_{t} S) \to \forall y \in x \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A)))$
67	66	ralrimiv	$⊢ (R \in LocallyA\landS \in LocallyA\to\forall x \in (R \times_{t} S) \forall y \in x \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A))$
68		islly	$⊢ R \times_{t} S \in LocallyA\leftrightarrow(R \times_{t} S \in Top \land \forall x \in (R \times_{t} S) \forall y \in x \exists z \in ((R \times_{t} S) \cap 𝒫 x) (y \in z \land (R \times_{t} S) ↾_{𝑡} z \in A))$
69	5 67 68	sylanbrc	$⊢ (R \in LocallyA\landS \in LocallyA\toR \times_{t} S \in LocallyA)$

Metamath Proof Explorer

Theorem txlly

Proof