cvmsdisj

Description: An even covering of U is a disjoint union. (Contributed by Mario Carneiro, 13-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	cvmsdisj	$⊢ (T \in S (U) \land A \in T \land B \in T) \to (A = B \lor A \cap B = \emptyset)$

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		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
3	1	cvmsi	$⊢ T \in S (U) \to (U \in J \land (T \subseteq C \land T \neq \emptyset) \land (⋃ T = F^{-1} [U] \land \forall u \in T (\forall v \in (T ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} U)))))$
4	3	simp3d	$⊢ T \in S (U) \to (⋃ T = F^{-1} [U] \land \forall u \in T (\forall v \in (T ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} U))))$
5	4	simprd	$⊢ T \in S (U) \to \forall u \in T (\forall v \in (T ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} U)))$
6		simpl	$⊢ (\forall v \in (T ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} U))) \to \forall v \in (T ∖ \{u\}) u \cap v = \emptyset$
7	6	ralimi	$⊢ \forall u \in T (\forall v \in (T ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} U))) \to \forall u \in T \forall v \in (T ∖ \{u\}) u \cap v = \emptyset$
8	5 7	syl	$⊢ T \in S (U) \to \forall u \in T \forall v \in (T ∖ \{u\}) u \cap v = \emptyset$
9		sneq	$⊢ u = A \to \{u\} = \{A\}$
10	9	difeq2d	$⊢ u = A \to T ∖ \{u\} = T ∖ \{A\}$
11		ineq1	$⊢ u = A \to u \cap v = A \cap v$
12	11	eqeq1d	$⊢ u = A \to (u \cap v = \emptyset \leftrightarrow A \cap v = \emptyset)$
13	10 12	raleqbidv	$⊢ u = A \to (\forall v \in (T ∖ \{u\}) u \cap v = \emptyset \leftrightarrow \forall v \in (T ∖ \{A\}) A \cap v = \emptyset)$
14	13	rspccva	$⊢ (\forall u \in T \forall v \in (T ∖ \{u\}) u \cap v = \emptyset \land A \in T) \to \forall v \in (T ∖ \{A\}) A \cap v = \emptyset$
15	8 14	sylan	$⊢ (T \in S (U) \land A \in T) \to \forall v \in (T ∖ \{A\}) A \cap v = \emptyset$
16		necom	$⊢ A \neq B \leftrightarrow B \neq A$
17		eldifsn	$⊢ B \in (T ∖ \{A\}) \leftrightarrow (B \in T \land B \neq A)$
18	17	biimpri	$⊢ (B \in T \land B \neq A) \to B \in (T ∖ \{A\})$
19	16 18	sylan2b	$⊢ (B \in T \land A \neq B) \to B \in (T ∖ \{A\})$
20		ineq2	$⊢ v = B \to A \cap v = A \cap B$
21	20	eqeq1d	$⊢ v = B \to (A \cap v = \emptyset \leftrightarrow A \cap B = \emptyset)$
22	21	rspccv	$⊢ \forall v \in (T ∖ \{A\}) A \cap v = \emptyset \to (B \in (T ∖ \{A\}) \to A \cap B = \emptyset)$
23	15 19 22	syl2im	$⊢ (T \in S (U) \land A \in T) \to ((B \in T \land A \neq B) \to A \cap B = \emptyset)$
24	23	expd	$⊢ (T \in S (U) \land A \in T) \to (B \in T \to (A \neq B \to A \cap B = \emptyset))$
25	24	3impia	$⊢ (T \in S (U) \land A \in T \land B \in T) \to (A \neq B \to A \cap B = \emptyset)$
26	2 25	biimtrrid	$⊢ (T \in S (U) \land A \in T \land B \in T) \to (\neg A = B \to A \cap B = \emptyset)$
27	26	orrd	$⊢ (T \in S (U) \land A \in T \land B \in T) \to (A = B \lor A \cap B = \emptyset)$

Metamath Proof Explorer

Theorem cvmsdisj

Proof