txnlly

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

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

Proof

Step	Hyp	Ref	Expression
1		txlly.1	$⊢ (j \in A \land k \in A) \to j \times_{t} k \in A$
2		nllytop	$⊢ R \in N-LocallyA\toR \in Top$
3		nllytop	$⊢ S \in N-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 N-LocallyA\landS \in N-LocallyA\toR \times_{t} S \in Top)$
6		eltx	$⊢ (R \in N-LocallyA\landS \in N-LocallyA\to(x \in (R \times_{t} S) \leftrightarrow \forall y \in x))$
7		simpll	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toR \in N-LocallyA))$
8		simprll	$⊢ ((R \in N-LocallyA\landS \in N-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 N-LocallyA\landS \in N-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 N-LocallyA\landS \in N-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		nlly2i	$⊢ (R \in N-LocallyA\landu \in R\land1^{st} (y) \in u\to\exists a \in 𝒫 u)$
13	7 8 11 12	syl3anc	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to\exists a \in 𝒫 u))$
14		simplr	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toS \in N-LocallyA))$
15		simprlr	$⊢ ((R \in N-LocallyA\landS \in N-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 N-LocallyA\landS \in N-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		nlly2i	$⊢ (S \in N-LocallyA\landv \in S\land2^{nd} (y) \in v\to\exists b \in 𝒫 v)$
19	14 15 17 18	syl3anc	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to\exists b \in 𝒫 v))$
20		reeanv	$⊢ \exists a \in 𝒫 u \exists b \in 𝒫 v (\exists r \in R (1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land \exists s \in S (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A)) \leftrightarrow (\exists a \in 𝒫 u \exists r \in R (1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land \exists b \in 𝒫 v \exists s \in S (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))$
21		reeanv	$⊢ \exists r \in R \exists s \in S ((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A)) \leftrightarrow (\exists r \in R (1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land \exists s \in S (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))$
22	5	ad3antrrr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toR \times_{t} S \in Top))))$
23	2	ad2antrr	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toR \in Top))$
24	23	ad2antrr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toR \in Top))))$
25	14 3	syl	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\toS \in Top))$
26	25	ad2antrr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toS \in Top))))$
27		simprrl	$⊢ (((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\tor \in R)))$
28	27	adantr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tor \in R))))$
29		simprrr	$⊢ (((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\tos \in S)))$
30	29	adantr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tos \in S))))$
31		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)$
32	24 26 28 30 31	syl22anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tor \times s \in (R \times_{t} S)))))$
33	9	ad2antrr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toy \in (u \times v)))))$
34		1st2nd2	$⊢ y \in (u \times v) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
35	33 34	syl	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toy = ⟨1^{st} (y), 2^{nd} (y)⟩))))$
36		simprl1	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to1^{st} (y) \in r))))$
37		simprr1	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to2^{nd} (y) \in s))))$
38	36 37	opelxpd	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to⟨1^{st} (y), 2^{nd} (y)⟩ \in (r \times s)))))$
39	35 38	eqeltrd	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toy \in (r \times s)))))$
40		opnneip	$⊢ (R \times_{t} S \in Top \land r \times s \in (R \times_{t} S) \land y \in (r \times s)) \to r \times s \in nei (R \times_{t} S) (\{y\})$
41	22 32 39 40	syl3anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tor \times s \in nei (R \times_{t} S) (\{y\})))))$
42		simprl2	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tor \subseteq a))))$
43		simprr2	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tos \subseteq b))))$
44		xpss12	$⊢ (r \subseteq a \land s \subseteq b) \to r \times s \subseteq a \times b$
45	42 43 44	syl2anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tor \times s \subseteq a \times b))))$
46		simprll	$⊢ (((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\toa \in 𝒫 u)))$
47	46	adantr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \in 𝒫 u))))$
48	47	elpwid	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \subseteq u))))$
49	8	ad2antrr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tou \in R))))$
50		elssuni	$⊢ u \in R \to u \subseteq ⋃ R$
51	49 50	syl	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tou \subseteq ⋃ R))))$
52	48 51	sstrd	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \subseteq ⋃ R))))$
53		simprlr	$⊢ (((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\tob \in 𝒫 v)))$
54	53	adantr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tob \in 𝒫 v))))$
55	54	elpwid	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tob \subseteq v))))$
56	15	ad2antrr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tov \in S))))$
57		elssuni	$⊢ v \in S \to v \subseteq ⋃ S$
58	56 57	syl	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tov \subseteq ⋃ S))))$
59	55 58	sstrd	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tob \subseteq ⋃ S))))$
60		xpss12	$⊢ (a \subseteq ⋃ R \land b \subseteq ⋃ S) \to a \times b \subseteq ⋃ R \times ⋃ S$
61	52 59 60	syl2anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \times b \subseteq ⋃ R \times ⋃ S))))$
62		eqid	$⊢ ⋃ R = ⋃ R$
63		eqid	$⊢ ⋃ S = ⋃ S$
64	62 63	txuni	$⊢ (R \in Top \land S \in Top) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
65	24 26 64	syl2anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to⋃ R \times ⋃ S = ⋃ (R \times_{t} S)))))$
66	61 65	sseqtrd	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \times b \subseteq ⋃ (R \times_{t} S)))))$
67		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
68	67	ssnei2	$⊢ ((R \times_{t} S \in Top \land r \times s \in nei (R \times_{t} S) (\{y\})) \land (r \times s \subseteq a \times b \land a \times b \subseteq ⋃ (R \times_{t} S))) \to a \times b \in nei (R \times_{t} S) (\{y\})$
69	22 41 45 66 68	syl22anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \times b \in nei (R \times_{t} S) (\{y\})))))$
70		xpss12	$⊢ (a \subseteq u \land b \subseteq v) \to a \times b \subseteq u \times v$
71	48 55 70	syl2anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \times b \subseteq u \times v))))$
72		simprrr	$⊢ ((R \in N-LocallyA\landS \in N-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))$
73	72	ad2antrr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\tou \times v \subseteq x))))$
74	71 73	sstrd	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \times b \subseteq x))))$
75		vex	$⊢ x \in V$
76	75	elpw2	$⊢ a \times b \in 𝒫 x \leftrightarrow a \times b \subseteq x$
77	74 76	sylibr	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \times b \in 𝒫 x))))$
78	69 77	elind	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toa \times b \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x)))))$
79		txrest	$⊢ ((R \in Top \land S \in Top) \land (a \in 𝒫 u \land b \in 𝒫 v)) \to (R \times_{t} S) ↾_{𝑡} (a \times b) = (R ↾_{𝑡} a) \times_{t} (S ↾_{𝑡} b)$
80	24 26 47 54 79	syl22anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to(R \times_{t} S) ↾_{𝑡} (a \times b) = (R ↾_{𝑡} a) \times_{t} (S ↾_{𝑡} b)))))$
81		simprl3	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toR ↾_{𝑡} a \in A))))$
82		simprr3	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\toS ↾_{𝑡} b \in A))))$
83	1	caovcl	$⊢ (R ↾_{𝑡} a \in A \land S ↾_{𝑡} b \in A) \to (R ↾_{𝑡} a) \times_{t} (S ↾_{𝑡} b) \in A$
84	81 82 83	syl2anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to(R ↾_{𝑡} a) \times_{t} (S ↾_{𝑡} b) \in A))))$
85	80 84	eqeltrd	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to(R \times_{t} S) ↾_{𝑡} (a \times b) \in A))))$
86		oveq2	$⊢ z = a \times b \to (R \times_{t} S) ↾_{𝑡} z = (R \times_{t} S) ↾_{𝑡} (a \times b)$
87	86	eleq1d	$⊢ z = a \times b \to ((R \times_{t} S) ↾_{𝑡} z \in A \leftrightarrow (R \times_{t} S) ↾_{𝑡} (a \times b) \in A)$
88	87	rspcev	$⊢ (a \times b \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x) \land (R \times_{t} S) ↾_{𝑡} (a \times b) \in A) \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x) (R \times_{t} S) ↾_{𝑡} z \in A$
89	78 85 88	syl2anc	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\land((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A))\to\exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x)))))$
90	89	ex	$⊢ (((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land((a \in 𝒫 u \land b \in 𝒫 v) \land (r \in R \land s \in S))\to(((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A)) \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x)))))$
91	90	anassrs	$⊢ ((((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land(a \in 𝒫 u \land b \in 𝒫 v)\land(r \in R \land s \in S)\to(((1^{st} (y) \in r \land r \subseteq a \land R ↾_{𝑡} a \in A) \land (2^{nd} (y) \in s \land s \subseteq b \land S ↾_{𝑡} b \in A)) \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x))))))$
92	91	rexlimdvva	$⊢ (((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land(a \in 𝒫 u \land b \in 𝒫 v)\to(\exists r \in R \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x)))))$
93	21 92	syl5bir	$⊢ (((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\land(a \in 𝒫 u \land b \in 𝒫 v)\to((\exists r \in R \land \exists s \in S) \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x)))))$
94	93	rexlimdvva	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to(\exists a \in 𝒫 u \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x))))$
95	20 94	syl5bir	$⊢ ((R \in N-LocallyA\landS \in N-LocallyA\land((u \in R \land v \in S) \land (y \in (u \times v) \land u \times v \subseteq x))\to((\exists a \in 𝒫 u \land \exists b \in 𝒫 v) \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x))))$
96	13 19 95	mp2and	$⊢ ((R \in N-LocallyA\landS \in N-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 (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x)))$
97	96	expr	$⊢ ((R \in N-LocallyA\landS \in N-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 (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x))))$
98	97	rexlimdvva	$⊢ (R \in N-LocallyA\landS \in N-LocallyA\to(\exists u \in R \to \exists z \in (nei (R \times_{t} S) (\{y\}) \cap 𝒫 x)))$
99	98	ralimdv	$⊢ (R \in N-LocallyA\landS \in N-LocallyA\to(\forall y \in x \to \forall y \in x))$
100	6 99	sylbid	$⊢ (R \in N-LocallyA\landS \in N-LocallyA\to(x \in (R \times_{t} S) \to \forall y \in x))$
101	100	ralrimiv	$⊢ (R \in N-LocallyA\landS \in N-LocallyA\to\forall x \in (R \times_{t} S))$
102		isnlly	$⊢ R \times_{t} S \in N-LocallyA\leftrightarrow(R \times_{t} S \in Top \land \forall x \in (R \times_{t} S))$
103	5 101 102	sylanbrc	$⊢ (R \in N-LocallyA\landS \in N-LocallyA\toR \times_{t} S \in N-LocallyA)$

Metamath Proof Explorer

Theorem txnlly

Proof