Metamath Proof Explorer

Theorem 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 ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
Assertion cvmsdisj ⊢ T ∈ S ⁡ U ∧ A ∈ T ∧ B ∈ T → A = B ∨ A ∩ B = ∅

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ S = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
2 df-ne ⊢ A ≠ B ↔ ¬ A = B
3 1 cvmsi ⊢ T ∈ S ⁡ U → U ∈ J ∧ T ⊆ C ∧ T ≠ ∅ ∧ ⋃ T = F -1 U ∧ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
4 3 simp3d ⊢ T ∈ S ⁡ U → ⋃ T = F -1 U ∧ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
5 4 simprd ⊢ T ∈ S ⁡ U → ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
6 simpl ⊢ ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U → ∀ v ∈ T ∖ u u ∩ v = ∅
7 6 ralimi ⊢ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U → ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅
8 5 7 syl ⊢ T ∈ S ⁡ U → ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅
9 sneq ⊢ u = A → u = A
10 9 difeq2d ⊢ u = A → T ∖ u = T ∖ A
11 ineq1 ⊢ u = A → u ∩ v = A ∩ v
12 11 eqeq1d ⊢ u = A → u ∩ v = ∅ ↔ A ∩ v = ∅
13 10 12 raleqbidv ⊢ u = A → ∀ v ∈ T ∖ u u ∩ v = ∅ ↔ ∀ v ∈ T ∖ A A ∩ v = ∅
14 13 rspccva ⊢ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ A ∈ T → ∀ v ∈ T ∖ A A ∩ v = ∅
15 8 14 sylan ⊢ T ∈ S ⁡ U ∧ A ∈ T → ∀ v ∈ T ∖ A A ∩ v = ∅
16 necom ⊢ A ≠ B ↔ B ≠ A
17 eldifsn ⊢ B ∈ T ∖ A ↔ B ∈ T ∧ B ≠ A
18 17 biimpri ⊢ B ∈ T ∧ B ≠ A → B ∈ T ∖ A
19 16 18 sylan2b ⊢ B ∈ T ∧ A ≠ B → B ∈ T ∖ A
20 ineq2 ⊢ v = B → A ∩ v = A ∩ B
21 20 eqeq1d ⊢ v = B → A ∩ v = ∅ ↔ A ∩ B = ∅
22 21 rspccv ⊢ ∀ v ∈ T ∖ A A ∩ v = ∅ → B ∈ T ∖ A → A ∩ B = ∅
23 15 19 22 syl2im ⊢ T ∈ S ⁡ U ∧ A ∈ T → B ∈ T ∧ A ≠ B → A ∩ B = ∅
24 23 expd ⊢ T ∈ S ⁡ U ∧ A ∈ T → B ∈ T → A ≠ B → A ∩ B = ∅
25 24 3impia ⊢ T ∈ S ⁡ U ∧ A ∈ T ∧ B ∈ T → A ≠ B → A ∩ B = ∅
26 2 25 syl5bir ⊢ T ∈ S ⁡ U ∧ A ∈ T ∧ B ∈ T → ¬ A = B → A ∩ B = ∅
27 26 orrd ⊢ T ∈ S ⁡ U ∧ A ∈ T ∧ B ∈ T → A = B ∨ A ∩ B = ∅