cvmfolem

	Ref	Expression
Hypotheses	cvmcov.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))))\})$
	cvmseu.1	$⊢ B = ⋃ C$
	cvmfolem.2	$⊢ X = ⋃ J$
Assertion	cvmfolem	$⊢ F \in (C CovMap J) \to F : B \underset{onto}{⟶} X$

Proof

Step	Hyp	Ref	Expression
1		cvmcov.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		cvmseu.1	$⊢ B = ⋃ C$
3		cvmfolem.2	$⊢ X = ⋃ J$
4		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
5	2 3	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ X$
6	4 5	syl	$⊢ F \in (C CovMap J) \to F : B ⟶ X$
7	1 3	cvmcov	$⊢ (F \in (C CovMap J) \land x \in X) \to \exists z \in J (x \in z \land S (z) \neq \emptyset)$
8	7	ex	$⊢ F \in (C CovMap J) \to (x \in X \to \exists z \in J (x \in z \land S (z) \neq \emptyset))$
9		n0	$⊢ S (z) \neq \emptyset \leftrightarrow \exists w w \in S (z)$
10	1	cvmsn0	$⊢ w \in S (z) \to w \neq \emptyset$
11	10	ad2antll	$⊢ ((F \in (C CovMap J) \land z \in J) \land (x \in z \land w \in S (z))) \to w \neq \emptyset$
12		n0	$⊢ w \neq \emptyset \leftrightarrow \exists t t \in w$
13	11 12	sylib	$⊢ ((F \in (C CovMap J) \land z \in J) \land (x \in z \land w \in S (z))) \to \exists t t \in w$
14		simprlr	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to w \in S (z)$
15	1	cvmsss	$⊢ w \in S (z) \to w \subseteq C$
16	14 15	syl	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to w \subseteq C$
17		simprr	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to t \in w$
18	16 17	sseldd	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to t \in C$
19		elssuni	$⊢ t \in C \to t \subseteq ⋃ C$
20	18 19	syl	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to t \subseteq ⋃ C$
21	20 2	sseqtrrdi	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to t \subseteq B$
22		simpll	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to F \in (C CovMap J)$
23	1	cvmsf1o	$⊢ (F \in (C CovMap J) \land w \in S (z) \land t \in w) \to ({F ↾}_{t}) : t \underset{1-1 onto}{⟶} z$
24	22 14 17 23	syl3anc	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to ({F ↾}_{t}) : t \underset{1-1 onto}{⟶} z$
25		f1ocnv	$⊢ ({F ↾}_{t}) : t \underset{1-1 onto}{⟶} z \to {({F ↾}_{t})}^{-1} : z \underset{1-1 onto}{⟶} t$
26		f1of	$⊢ {({F ↾}_{t})}^{-1} : z \underset{1-1 onto}{⟶} t \to {({F ↾}_{t})}^{-1} : z ⟶ t$
27	24 25 26	3syl	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to {({F ↾}_{t})}^{-1} : z ⟶ t$
28		simprll	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to x \in z$
29	27 28	ffvelrnd	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to {({F ↾}_{t})}^{-1} (x) \in t$
30	21 29	sseldd	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to {({F ↾}_{t})}^{-1} (x) \in B$
31		f1ocnvfv2	$⊢ (({F ↾}_{t}) : t \underset{1-1 onto}{⟶} z \land x \in z) \to ({F ↾}_{t}) ({({F ↾}_{t})}^{-1} (x)) = x$
32	24 28 31	syl2anc	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to ({F ↾}_{t}) ({({F ↾}_{t})}^{-1} (x)) = x$
33		fvres	$⊢ {({F ↾}_{t})}^{-1} (x) \in t \to ({F ↾}_{t}) ({({F ↾}_{t})}^{-1} (x)) = F ({({F ↾}_{t})}^{-1} (x))$
34	29 33	syl	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to ({F ↾}_{t}) ({({F ↾}_{t})}^{-1} (x)) = F ({({F ↾}_{t})}^{-1} (x))$
35	32 34	eqtr3d	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to x = F ({({F ↾}_{t})}^{-1} (x))$
36		fveq2	$⊢ y = {({F ↾}_{t})}^{-1} (x) \to F (y) = F ({({F ↾}_{t})}^{-1} (x))$
37	36	rspceeqv	$⊢ ({({F ↾}_{t})}^{-1} (x) \in B \land x = F ({({F ↾}_{t})}^{-1} (x))) \to \exists y \in B x = F (y)$
38	30 35 37	syl2anc	$⊢ ((F \in (C CovMap J) \land z \in J) \land ((x \in z \land w \in S (z)) \land t \in w)) \to \exists y \in B x = F (y)$
39	38	expr	$⊢ ((F \in (C CovMap J) \land z \in J) \land (x \in z \land w \in S (z))) \to (t \in w \to \exists y \in B x = F (y))$
40	39	exlimdv	$⊢ ((F \in (C CovMap J) \land z \in J) \land (x \in z \land w \in S (z))) \to (\exists t t \in w \to \exists y \in B x = F (y))$
41	13 40	mpd	$⊢ ((F \in (C CovMap J) \land z \in J) \land (x \in z \land w \in S (z))) \to \exists y \in B x = F (y)$
42	41	expr	$⊢ ((F \in (C CovMap J) \land z \in J) \land x \in z) \to (w \in S (z) \to \exists y \in B x = F (y))$
43	42	exlimdv	$⊢ ((F \in (C CovMap J) \land z \in J) \land x \in z) \to (\exists w w \in S (z) \to \exists y \in B x = F (y))$
44	9 43	syl5bi	$⊢ ((F \in (C CovMap J) \land z \in J) \land x \in z) \to (S (z) \neq \emptyset \to \exists y \in B x = F (y))$
45	44	expimpd	$⊢ (F \in (C CovMap J) \land z \in J) \to ((x \in z \land S (z) \neq \emptyset) \to \exists y \in B x = F (y))$
46	45	rexlimdva	$⊢ F \in (C CovMap J) \to (\exists z \in J (x \in z \land S (z) \neq \emptyset) \to \exists y \in B x = F (y))$
47	8 46	syld	$⊢ F \in (C CovMap J) \to (x \in X \to \exists y \in B x = F (y))$
48	47	ralrimiv	$⊢ F \in (C CovMap J) \to \forall x \in X \exists y \in B x = F (y)$
49		dffo3	$⊢ F : B \underset{onto}{⟶} X \leftrightarrow (F : B ⟶ X \land \forall x \in X \exists y \in B x = F (y))$
50	6 48 49	sylanbrc	$⊢ F \in (C CovMap J) \to F : B \underset{onto}{⟶} X$

Metamath Proof Explorer

Theorem cvmfolem

Proof