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 e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
Assertion cvmsdisj 
|- ( ( T e. ( S ` U ) /\ A e. T /\ B e. T ) -> ( A = B \/ ( A i^i B ) = (/) ) )

Proof

Step Hyp Ref Expression
1 cvmcov.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 df-ne 
 |-  ( A =/= B <-> -. A = B )
3 1 cvmsi 
 |-  ( T e. ( S ` U ) -> ( U e. J /\ ( T C_ C /\ T =/= (/) ) /\ ( U. T = ( `' F " U ) /\ A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) ) )
4 3 simp3d 
 |-  ( T e. ( S ` U ) -> ( U. T = ( `' F " U ) /\ A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) )
5 4 simprd 
 |-  ( T e. ( S ` U ) -> A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) )
6 simpl 
 |-  ( ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) -> A. v e. ( T \ { u } ) ( u i^i v ) = (/) )
7 6 ralimi 
 |-  ( A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) -> A. u e. T A. v e. ( T \ { u } ) ( u i^i v ) = (/) )
8 5 7 syl 
 |-  ( T e. ( S ` U ) -> A. u e. T A. v e. ( T \ { u } ) ( u i^i v ) = (/) )
9 sneq 
 |-  ( u = A -> { u } = { A } )
10 9 difeq2d 
 |-  ( u = A -> ( T \ { u } ) = ( T \ { A } ) )
11 ineq1 
 |-  ( u = A -> ( u i^i v ) = ( A i^i v ) )
12 11 eqeq1d 
 |-  ( u = A -> ( ( u i^i v ) = (/) <-> ( A i^i v ) = (/) ) )
13 10 12 raleqbidv 
 |-  ( u = A -> ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) <-> A. v e. ( T \ { A } ) ( A i^i v ) = (/) ) )
14 13 rspccva 
 |-  ( ( A. u e. T A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ A e. T ) -> A. v e. ( T \ { A } ) ( A i^i v ) = (/) )
15 8 14 sylan 
 |-  ( ( T e. ( S ` U ) /\ A e. T ) -> A. v e. ( T \ { A } ) ( A i^i v ) = (/) )
16 necom 
 |-  ( A =/= B <-> B =/= A )
17 eldifsn 
 |-  ( B e. ( T \ { A } ) <-> ( B e. T /\ B =/= A ) )
18 17 biimpri 
 |-  ( ( B e. T /\ B =/= A ) -> B e. ( T \ { A } ) )
19 16 18 sylan2b 
 |-  ( ( B e. T /\ A =/= B ) -> B e. ( T \ { A } ) )
20 ineq2 
 |-  ( v = B -> ( A i^i v ) = ( A i^i B ) )
21 20 eqeq1d 
 |-  ( v = B -> ( ( A i^i v ) = (/) <-> ( A i^i B ) = (/) ) )
22 21 rspccv 
 |-  ( A. v e. ( T \ { A } ) ( A i^i v ) = (/) -> ( B e. ( T \ { A } ) -> ( A i^i B ) = (/) ) )
23 15 19 22 syl2im 
 |-  ( ( T e. ( S ` U ) /\ A e. T ) -> ( ( B e. T /\ A =/= B ) -> ( A i^i B ) = (/) ) )
24 23 expd 
 |-  ( ( T e. ( S ` U ) /\ A e. T ) -> ( B e. T -> ( A =/= B -> ( A i^i B ) = (/) ) ) )
25 24 3impia 
 |-  ( ( T e. ( S ` U ) /\ A e. T /\ B e. T ) -> ( A =/= B -> ( A i^i B ) = (/) ) )
26 2 25 syl5bir 
 |-  ( ( T e. ( S ` U ) /\ A e. T /\ B e. T ) -> ( -. A = B -> ( A i^i B ) = (/) ) )
27 26 orrd 
 |-  ( ( T e. ( S ` U ) /\ A e. T /\ B e. T ) -> ( A = B \/ ( A i^i B ) = (/) ) )