cvmseu

Description: Every element in U. T is a member of a unique element of T . (Contributed by Mario Carneiro, 14-Feb-2015)

	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$
Assertion	cvmseu	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to \exists! x \in T A \in 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		simpr2	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to A \in B$
4		simpr3	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to F (A) \in U$
5		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
6	5	adantr	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to F \in (C Cn J)$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	2 7	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
9		ffn	$⊢ F : B ⟶ ⋃ J \to F Fn B$
10		elpreima	$⊢ F Fn B \to (A \in F^{-1} [U] \leftrightarrow (A \in B \land F (A) \in U))$
11	6 8 9 10	4syl	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to (A \in F^{-1} [U] \leftrightarrow (A \in B \land F (A) \in U))$
12	3 4 11	mpbir2and	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to A \in F^{-1} [U]$
13		simpr1	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to T \in S (U)$
14	1	cvmsuni	$⊢ T \in S (U) \to ⋃ T = F^{-1} [U]$
15	13 14	syl	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to ⋃ T = F^{-1} [U]$
16	12 15	eleqtrrd	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to A \in ⋃ T$
17		eluni2	$⊢ A \in ⋃ T \leftrightarrow \exists x \in T A \in x$
18	16 17	sylib	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to \exists x \in T A \in x$
19		inelcm	$⊢ (A \in x \land A \in z) \to x \cap z \neq \emptyset$
20	1	cvmsdisj	$⊢ (T \in S (U) \land x \in T \land z \in T) \to (x = z \lor x \cap z = \emptyset)$
21	20	3expb	$⊢ (T \in S (U) \land (x \in T \land z \in T)) \to (x = z \lor x \cap z = \emptyset)$
22	13 21	sylan	$⊢ ((F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \land (x \in T \land z \in T)) \to (x = z \lor x \cap z = \emptyset)$
23	22	ord	$⊢ ((F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \land (x \in T \land z \in T)) \to (\neg x = z \to x \cap z = \emptyset)$
24	23	necon1ad	$⊢ ((F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \land (x \in T \land z \in T)) \to (x \cap z \neq \emptyset \to x = z)$
25	19 24	syl5	$⊢ ((F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \land (x \in T \land z \in T)) \to ((A \in x \land A \in z) \to x = z)$
26	25	ralrimivva	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to \forall x \in T \forall z \in T ((A \in x \land A \in z) \to x = z)$
27		eleq2w	$⊢ x = z \to (A \in x \leftrightarrow A \in z)$
28	27	reu4	$⊢ \exists! x \in T A \in x \leftrightarrow (\exists x \in T A \in x \land \forall x \in T \forall z \in T ((A \in x \land A \in z) \to x = z))$
29	18 26 28	sylanbrc	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to \exists! x \in T A \in x$

Metamath Proof Explorer

Theorem cvmseu

Proof