ismntop

Description: Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020)

		Ref	Expression
	Assertion	ismntop	$⊢ (N \in ℕ_{0} \land J \in V) \to (N ManTop J \leftrightarrow (J \in 2^{nd} 𝜔 \land J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N)))))$

Proof

Step	Hyp	Ref	Expression
1		ismntoplly	$⊢ (N \in ℕ_{0} \land J \in V) \to (N ManTop J \leftrightarrow (J \in 2^{nd} 𝜔 \land J \in Haus \land J \in Locally[TopOpen (𝔼_{hil} (N))] ≃))$
2		haustop	$⊢ J \in Haus \to J \in Top$
3	2	adantl	$⊢ (N \in ℕ_{0} \land J \in Haus) \to J \in Top$
4	3	biantrurd	$⊢ (N \in ℕ_{0} \land J \in Haus) \to (\forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃) \leftrightarrow (J \in Top \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃)))$
5		hmpher	$⊢ ≃ Er Top$
6		errel	$⊢ ≃ Er Top \to Rel ≃$
7		relelec	$⊢ Rel ≃ \to (J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃ \leftrightarrow TopOpen (𝔼_{hil} (N)) ≃ (J ↾_{𝑡} u))$
8	5 6 7	mp2b	$⊢ J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃ \leftrightarrow TopOpen (𝔼_{hil} (N)) ≃ (J ↾_{𝑡} u)$
9		hmphsymb	$⊢ TopOpen (𝔼_{hil} (N)) ≃ (J ↾_{𝑡} u) \leftrightarrow (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))$
10	8 9	bitr2i	$⊢ (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N)) \leftrightarrow J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃$
11	10	a1i	$⊢ (N \in ℕ_{0} \land J \in Haus) \to ((J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N)) \leftrightarrow J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃)$
12	11	anbi2d	$⊢ (N \in ℕ_{0} \land J \in Haus) \to ((y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))) \leftrightarrow (y \in u \land J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃))$
13	12	rexbidv	$⊢ (N \in ℕ_{0} \land J \in Haus) \to (\exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))) \leftrightarrow \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃))$
14	13	2ralbidv	$⊢ (N \in ℕ_{0} \land J \in Haus) \to (\forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))) \leftrightarrow \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃))$
15		islly	$⊢ J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow(J \in Top \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃))$
16	15	a1i	$⊢ (N \in ℕ_{0} \land J \in Haus) \to (J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow(J \in Top \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in [TopOpen (𝔼_{hil} (N))] ≃)))$
17	4 14 16	3bitr4rd	$⊢ (N \in ℕ_{0} \land J \in Haus) \to (J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow\forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))))$
18	17	pm5.32da	$⊢ N \in ℕ_{0} \to ((J \in Haus \land J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow(J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))))))$
19	18	anbi2d	$⊢ N \in ℕ_{0} \to ((J \in 2^{nd} 𝜔 \land (J \in Haus \land J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow(J \in 2^{nd} 𝜔 \land (J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))))))))$
20		3anass	$⊢ (J \in 2^{nd} 𝜔 \land J \in Haus \land J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow(J \in 2^{nd} 𝜔 \land (J \in Haus \land J \in Locally[TopOpen (𝔼_{hil} (N))] ≃)))$
21		3anass	$⊢ (J \in 2^{nd} 𝜔 \land J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N)))) \leftrightarrow (J \in 2^{nd} 𝜔 \land (J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N)))))$
22	19 20 21	3bitr4g	$⊢ N \in ℕ_{0} \to ((J \in 2^{nd} 𝜔 \land J \in Haus \land J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow(J \in 2^{nd} 𝜔 \land J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))))))$
23	22	adantr	$⊢ (N \in ℕ_{0} \land J \in V) \to ((J \in 2^{nd} 𝜔 \land J \in Haus \land J \in Locally[TopOpen (𝔼_{hil} (N))] ≃\leftrightarrow(J \in 2^{nd} 𝜔 \land J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N))))))$
24	1 23	bitrd	$⊢ (N \in ℕ_{0} \land J \in V) \to (N ManTop J \leftrightarrow (J \in 2^{nd} 𝜔 \land J \in Haus \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land (J ↾_{𝑡} u) ≃ TopOpen (𝔼_{hil} (N)))))$

Metamath Proof Explorer

Theorem ismntop

Proof