llyi

Description: The property of a locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	llyi	$⊢ (J \in LocallyA\landU \in J\landP \in U\to\exists u \in J)$

Proof

Step	Hyp	Ref	Expression
1		islly	$⊢ J \in LocallyA\leftrightarrow(J \in Top \land \forall x \in J)$
2	1	simprbi	$⊢ J \in LocallyA\to\forall x \in J$
3		pweq	$⊢ x = U \to 𝒫 x = 𝒫 U$
4	3	ineq2d	$⊢ x = U \to J \cap 𝒫 x = J \cap 𝒫 U$
5	4	rexeqdv	$⊢ x = U \to (\exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in A) \leftrightarrow \exists u \in (J \cap 𝒫 U) (y \in u \land J ↾_{𝑡} u \in A))$
6	5	raleqbi1dv	$⊢ x = U \to (\forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in A) \leftrightarrow \forall y \in U \exists u \in (J \cap 𝒫 U) (y \in u \land J ↾_{𝑡} u \in A))$
7	6	rspccva	$⊢ (\forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in A) \land U \in J) \to \forall y \in U \exists u \in (J \cap 𝒫 U) (y \in u \land J ↾_{𝑡} u \in A)$
8	2 7	sylan	$⊢ (J \in LocallyA\landU \in J\to\forall y \in U)$
9		eleq1	$⊢ y = P \to (y \in u \leftrightarrow P \in u)$
10	9	anbi1d	$⊢ y = P \to ((y \in u \land J ↾_{𝑡} u \in A) \leftrightarrow (P \in u \land J ↾_{𝑡} u \in A))$
11	10	anbi2d	$⊢ y = P \to ((u \in (J \cap 𝒫 U) \land (y \in u \land J ↾_{𝑡} u \in A)) \leftrightarrow (u \in (J \cap 𝒫 U) \land (P \in u \land J ↾_{𝑡} u \in A)))$
12		anass	$⊢ ((u \in J \land u \subseteq U) \land (P \in u \land J ↾_{𝑡} u \in A)) \leftrightarrow (u \in J \land (u \subseteq U \land (P \in u \land J ↾_{𝑡} u \in A)))$
13		elin	$⊢ u \in (J \cap 𝒫 U) \leftrightarrow (u \in J \land u \in 𝒫 U)$
14		velpw	$⊢ u \in 𝒫 U \leftrightarrow u \subseteq U$
15	14	anbi2i	$⊢ (u \in J \land u \in 𝒫 U) \leftrightarrow (u \in J \land u \subseteq U)$
16	13 15	bitri	$⊢ u \in (J \cap 𝒫 U) \leftrightarrow (u \in J \land u \subseteq U)$
17	16	anbi1i	$⊢ (u \in (J \cap 𝒫 U) \land (P \in u \land J ↾_{𝑡} u \in A)) \leftrightarrow ((u \in J \land u \subseteq U) \land (P \in u \land J ↾_{𝑡} u \in A))$
18		3anass	$⊢ (u \subseteq U \land P \in u \land J ↾_{𝑡} u \in A) \leftrightarrow (u \subseteq U \land (P \in u \land J ↾_{𝑡} u \in A))$
19	18	anbi2i	$⊢ (u \in J \land (u \subseteq U \land P \in u \land J ↾_{𝑡} u \in A)) \leftrightarrow (u \in J \land (u \subseteq U \land (P \in u \land J ↾_{𝑡} u \in A)))$
20	12 17 19	3bitr4i	$⊢ (u \in (J \cap 𝒫 U) \land (P \in u \land J ↾_{𝑡} u \in A)) \leftrightarrow (u \in J \land (u \subseteq U \land P \in u \land J ↾_{𝑡} u \in A))$
21	11 20	bitrdi	$⊢ y = P \to ((u \in (J \cap 𝒫 U) \land (y \in u \land J ↾_{𝑡} u \in A)) \leftrightarrow (u \in J \land (u \subseteq U \land P \in u \land J ↾_{𝑡} u \in A)))$
22	21	rexbidv2	$⊢ y = P \to (\exists u \in (J \cap 𝒫 U) (y \in u \land J ↾_{𝑡} u \in A) \leftrightarrow \exists u \in J (u \subseteq U \land P \in u \land J ↾_{𝑡} u \in A))$
23	22	rspccva	$⊢ (\forall y \in U \exists u \in (J \cap 𝒫 U) (y \in u \land J ↾_{𝑡} u \in A) \land P \in U) \to \exists u \in J (u \subseteq U \land P \in u \land J ↾_{𝑡} u \in A)$
24	8 23	stoic3	$⊢ (J \in LocallyA\landU \in J\landP \in U\to\exists u \in J)$

Metamath Proof Explorer

Theorem llyi

Proof