iscvm

Description: The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	iscvm.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	iscvm.2	$⊢ X = ⋃ J$
Assertion	iscvm	$⊢ F \in (C CovMap J) \leftrightarrow ((C \in Top \land J \in Top \land F \in (C Cn J)) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		iscvm.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		iscvm.2	$⊢ X = ⋃ J$
3		anass	$⊢ (((C \in Top \land J \in Top) \land F \in (C Cn J)) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)) \leftrightarrow ((C \in Top \land J \in Top) \land (F \in (C Cn J) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)))$
4		df-3an	$⊢ (C \in Top \land J \in Top \land F \in (C Cn J)) \leftrightarrow ((C \in Top \land J \in Top) \land F \in (C Cn J))$
5	4	anbi1i	$⊢ ((C \in Top \land J \in Top \land F \in (C Cn J)) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)) \leftrightarrow (((C \in Top \land J \in Top) \land F \in (C Cn J)) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset))$
6		df-cvm	$⊢ CovMap = (c \in Top, j \in Top ⟼ \{f \in (c Cn j) \| \forall x \in ⋃ j \exists k \in j (x \in k \land \exists s \in (𝒫 c ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k)))))\})$
7	6	elmpocl	$⊢ F \in (C CovMap J) \to (C \in Top \land J \in Top)$
8		oveq12	$⊢ (c = C \land j = J) \to c Cn j = C Cn J$
9		simpr	$⊢ (c = C \land j = J) \to j = J$
10	9	unieqd	$⊢ (c = C \land j = J) \to ⋃ j = ⋃ J$
11	10 2	eqtr4di	$⊢ (c = C \land j = J) \to ⋃ j = X$
12		simpl	$⊢ (c = C \land j = J) \to c = C$
13	12	pweqd	$⊢ (c = C \land j = J) \to 𝒫 c = 𝒫 C$
14	13	difeq1d	$⊢ (c = C \land j = J) \to 𝒫 c ∖ \{\emptyset\} = 𝒫 C ∖ \{\emptyset\}$
15		oveq1	$⊢ c = C \to c ↾_{𝑡} u = C ↾_{𝑡} u$
16		oveq1	$⊢ j = J \to j ↾_{𝑡} k = J ↾_{𝑡} k$
17	15 16	oveqan12d	$⊢ (c = C \land j = J) \to (c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k) = (C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)$
18	17	eleq2d	$⊢ (c = C \land j = J) \to ({f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k)) \leftrightarrow {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))$
19	18	anbi2d	$⊢ (c = C \land j = J) \to ((\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k))) \leftrightarrow (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))$
20	19	ralbidv	$⊢ (c = C \land j = J) \to (\forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k))) \leftrightarrow \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))$
21	20	anbi2d	$⊢ (c = C \land j = J) \to ((⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k)))) \leftrightarrow (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))$
22	14 21	rexeqbidv	$⊢ (c = C \land j = J) \to (\exists s \in (𝒫 c ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k)))) \leftrightarrow \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))$
23	22	anbi2d	$⊢ (c = C \land j = J) \to ((x \in k \land \exists s \in (𝒫 c ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k))))) \leftrightarrow (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
24	9 23	rexeqbidv	$⊢ (c = C \land j = J) \to (\exists k \in j (x \in k \land \exists s \in (𝒫 c ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k))))) \leftrightarrow \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
25	11 24	raleqbidv	$⊢ (c = C \land j = J) \to (\forall x \in ⋃ j \exists k \in j (x \in k \land \exists s \in (𝒫 c ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k))))) \leftrightarrow \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
26	8 25	rabeqbidv	$⊢ (c = C \land j = J) \to \{f \in (c Cn j) \| \forall x \in ⋃ j \exists k \in j (x \in k \land \exists s \in (𝒫 c ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((c ↾_{𝑡} u) Homeo (j ↾_{𝑡} k)))))\} = \{f \in (C Cn J) \| \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))\}$
27		ovex	$⊢ C Cn J \in V$
28	27	rabex	$⊢ \{f \in (C Cn J) \| \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))\} \in V$
29	26 6 28	ovmpoa	$⊢ (C \in Top \land J \in Top) \to C CovMap J = \{f \in (C Cn J) \| \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))\}$
30	29	eleq2d	$⊢ (C \in Top \land J \in Top) \to (F \in (C CovMap J) \leftrightarrow F \in \{f \in (C Cn J) \| \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))\})$
31		id	$⊢ k \in J \to k \in J$
32		pwexg	$⊢ C \in Top \to 𝒫 C \in V$
33	32	adantr	$⊢ (C \in Top \land J \in Top) \to 𝒫 C \in V$
34		difexg	$⊢ 𝒫 C \in V \to 𝒫 C ∖ \{\emptyset\} \in V$
35		rabexg	$⊢ 𝒫 C ∖ \{\emptyset\} \in V \to \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\} \in V$
36	33 34 35	3syl	$⊢ (C \in Top \land J \in Top) \to \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\} \in V$
37	1	fvmpt2	$⊢ (k \in J \land \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\} \in V) \to S (k) = \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\}$
38	31 36 37	syl2anr	$⊢ ((C \in Top \land J \in Top) \land k \in J) \to S (k) = \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\}$
39	38	neeq1d	$⊢ ((C \in Top \land J \in Top) \land k \in J) \to (S (k) \neq \emptyset \leftrightarrow \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\} \neq \emptyset)$
40		rabn0	$⊢ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\} \neq \emptyset \leftrightarrow \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))$
41	39 40	bitrdi	$⊢ ((C \in Top \land J \in Top) \land k \in J) \to (S (k) \neq \emptyset \leftrightarrow \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))$
42	41	anbi2d	$⊢ ((C \in Top \land J \in Top) \land k \in J) \to ((x \in k \land S (k) \neq \emptyset) \leftrightarrow (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
43	42	rexbidva	$⊢ (C \in Top \land J \in Top) \to (\exists k \in J (x \in k \land S (k) \neq \emptyset) \leftrightarrow \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
44	43	ralbidv	$⊢ (C \in Top \land J \in Top) \to (\forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset) \leftrightarrow \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
45	44	anbi2d	$⊢ (C \in Top \land J \in Top) \to ((F \in (C Cn J) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)) \leftrightarrow (F \in (C Cn J) \land \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))))$
46		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
47	46	imaeq1d	$⊢ f = F \to f^{-1} [k] = F^{-1} [k]$
48	47	eqeq2d	$⊢ f = F \to (⋃ s = f^{-1} [k] \leftrightarrow ⋃ s = F^{-1} [k])$
49		reseq1	$⊢ f = F \to {f ↾}_{u} = {F ↾}_{u}$
50	49	eleq1d	$⊢ f = F \to ({f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)) \leftrightarrow {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))$
51	50	anbi2d	$⊢ f = F \to ((\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))) \leftrightarrow (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))$
52	51	ralbidv	$⊢ f = F \to (\forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))) \leftrightarrow \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))$
53	48 52	anbi12d	$⊢ f = F \to ((⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))) \leftrightarrow (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))$
54	53	rexbidv	$⊢ f = F \to (\exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))) \leftrightarrow \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))$
55	54	anbi2d	$⊢ f = F \to ((x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))) \leftrightarrow (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
56	55	rexbidv	$⊢ f = F \to (\exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))) \leftrightarrow \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
57	56	ralbidv	$⊢ f = F \to (\forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))) \leftrightarrow \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
58	57	elrab	$⊢ F \in \{f \in (C Cn J) \| \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))\} \leftrightarrow (F \in (C Cn J) \land \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))))$
59	45 58	bitr4di	$⊢ (C \in Top \land J \in Top) \to ((F \in (C Cn J) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)) \leftrightarrow F \in \{f \in (C Cn J) \| \forall x \in X \exists k \in J (x \in k \land \exists s \in (𝒫 C ∖ \{\emptyset\}) (⋃ s = f^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {f ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k)))))\})$
60	30 59	bitr4d	$⊢ (C \in Top \land J \in Top) \to (F \in (C CovMap J) \leftrightarrow (F \in (C Cn J) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)))$
61	7 60	biadanii	$⊢ F \in (C CovMap J) \leftrightarrow ((C \in Top \land J \in Top) \land (F \in (C Cn J) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)))$
62	3 5 61	3bitr4ri	$⊢ F \in (C CovMap J) \leftrightarrow ((C \in Top \land J \in Top \land F \in (C Cn J)) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset))$

Metamath Proof Explorer

Theorem iscvm

Proof