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 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmsdisj ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 df-ne ⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
3 1 cvmsi ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑈 ∈ 𝐽 ∧ ( 𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅ ) ∧ ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )
4 3 simp3d ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) )
5 4 simprd ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) )
6 simpl ⊢ ( ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) → ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
7 6 ralimi ⊢ ( ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) → ∀ 𝑢 ∈ 𝑇 ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
8 5 7 syl ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∀ 𝑢 ∈ 𝑇 ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
9 sneq ⊢ ( 𝑢 = 𝐴 → { 𝑢 } = { 𝐴 } )
10 9 difeq2d ⊢ ( 𝑢 = 𝐴 → ( 𝑇 ∖ { 𝑢 } ) = ( 𝑇 ∖ { 𝐴 } ) )
11 ineq1 ⊢ ( 𝑢 = 𝐴 → ( 𝑢 ∩ 𝑣 ) = ( 𝐴 ∩ 𝑣 ) )
12 11 eqeq1d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( 𝐴 ∩ 𝑣 ) = ∅ ) )
13 10 12 raleqbidv ⊢ ( 𝑢 = 𝐴 → ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑣 ) = ∅ ) )
14 13 rspccva ⊢ ( ( ∀ 𝑢 ∈ 𝑇 ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ 𝐴 ∈ 𝑇 ) → ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑣 ) = ∅ )
15 8 14 sylan ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑣 ) = ∅ )
16 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
17 eldifsn ⊢ ( 𝐵 ∈ ( 𝑇 ∖ { 𝐴 } ) ↔ ( 𝐵 ∈ 𝑇 ∧ 𝐵 ≠ 𝐴 ) )
18 17 biimpri ⊢ ( ( 𝐵 ∈ 𝑇 ∧ 𝐵 ≠ 𝐴 ) → 𝐵 ∈ ( 𝑇 ∖ { 𝐴 } ) )
19 16 18 sylan2b ⊢ ( ( 𝐵 ∈ 𝑇 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝑇 ∖ { 𝐴 } ) )
20 ineq2 ⊢ ( 𝑣 = 𝐵 → ( 𝐴 ∩ 𝑣 ) = ( 𝐴 ∩ 𝐵 ) )
21 20 eqeq1d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ∩ 𝑣 ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
22 21 rspccv ⊢ ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑣 ) = ∅ → ( 𝐵 ∈ ( 𝑇 ∖ { 𝐴 } ) → ( 𝐴 ∩ 𝐵 ) = ∅ ) )
23 15 19 22 syl2im ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ( 𝐵 ∈ 𝑇 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = ∅ ) )
24 23 expd ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐵 ∈ 𝑇 → ( 𝐴 ≠ 𝐵 → ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
25 24 3impia ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 ≠ 𝐵 → ( 𝐴 ∩ 𝐵 ) = ∅ ) )
26 2 25 biimtrrid ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( ¬ 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = ∅ ) )
27 26 orrd ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )