cvmsf1o

Description: F , localized to an element of an even covering of U , is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015)

		Ref	Expression
	Hypothesis	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))))\})$
	Assertion	cvmsf1o	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} U$

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		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
3	2	3ad2ant1	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to C \in Top$
4		eqid	$⊢ ⋃ C = ⋃ C$
5	4	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (⋃ C)$
6	3 5	sylib	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to C \in TopOn (⋃ C)$
7	1	cvmsss	$⊢ T \in S (U) \to T \subseteq C$
8	7	3ad2ant2	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to T \subseteq C$
9		simp3	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to A \in T$
10	8 9	sseldd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to A \in C$
11		elssuni	$⊢ A \in C \to A \subseteq ⋃ C$
12	10 11	syl	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to A \subseteq ⋃ C$
13		resttopon	$⊢ (C \in TopOn (⋃ C) \land A \subseteq ⋃ C) \to C ↾_{𝑡} A \in TopOn (A)$
14	6 12 13	syl2anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to C ↾_{𝑡} A \in TopOn (A)$
15		cvmtop2	$⊢ F \in (C CovMap J) \to J \in Top$
16	15	3ad2ant1	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to J \in Top$
17		eqid	$⊢ ⋃ J = ⋃ J$
18	17	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
19	16 18	sylib	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to J \in TopOn (⋃ J)$
20	1	cvmsrcl	$⊢ T \in S (U) \to U \in J$
21	20	3ad2ant2	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to U \in J$
22		elssuni	$⊢ U \in J \to U \subseteq ⋃ J$
23	21 22	syl	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to U \subseteq ⋃ J$
24		resttopon	$⊢ (J \in TopOn (⋃ J) \land U \subseteq ⋃ J) \to J ↾_{𝑡} U \in TopOn (U)$
25	19 23 24	syl2anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to J ↾_{𝑡} U \in TopOn (U)$
26	1	cvmshmeo	$⊢ (T \in S (U) \land A \in T) \to {F ↾}_{A} \in ((C ↾_{𝑡} A) Homeo (J ↾_{𝑡} U))$
27	26	3adant1	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to {F ↾}_{A} \in ((C ↾_{𝑡} A) Homeo (J ↾_{𝑡} U))$
28		hmeof1o2	$⊢ (C ↾_{𝑡} A \in TopOn (A) \land J ↾_{𝑡} U \in TopOn (U) \land {F ↾}_{A} \in ((C ↾_{𝑡} A) Homeo (J ↾_{𝑡} U))) \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} U$
29	14 25 27 28	syl3anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} U$

Metamath Proof Explorer

Theorem cvmsf1o

Proof