Metamath Proof Explorer

Theorem 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 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 ) ) ) ) } )
cvmseu.1 
|- B = U. C
Assertion cvmseu 
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> E! x e. T A e. x )

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 cvmseu.1 
 |-  B = U. C
3 simpr2 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A e. B )
4 simpr3 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> ( F ` A ) e. U )
5 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
6 5 adantr 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> F e. ( C Cn J ) )
7 eqid 
 |-  U. J = U. J
8 2 7 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
9 ffn 
 |-  ( F : B --> U. J -> F Fn B )
10 elpreima 
 |-  ( F Fn B -> ( A e. ( `' F " U ) <-> ( A e. B /\ ( F ` A ) e. U ) ) )
11 6 8 9 10 4syl 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> ( A e. ( `' F " U ) <-> ( A e. B /\ ( F ` A ) e. U ) ) )
12 3 4 11 mpbir2and 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A e. ( `' F " U ) )
13 simpr1 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> T e. ( S ` U ) )
14 1 cvmsuni 
 |-  ( T e. ( S ` U ) -> U. T = ( `' F " U ) )
15 13 14 syl 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> U. T = ( `' F " U ) )
16 12 15 eleqtrrd 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A e. U. T )
17 eluni2 
 |-  ( A e. U. T <-> E. x e. T A e. x )
18 16 17 sylib 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> E. x e. T A e. x )
19 inelcm 
 |-  ( ( A e. x /\ A e. z ) -> ( x i^i z ) =/= (/) )
20 1 cvmsdisj 
 |-  ( ( T e. ( S ` U ) /\ x e. T /\ z e. T ) -> ( x = z \/ ( x i^i z ) = (/) ) )
21 20 3expb 
 |-  ( ( T e. ( S ` U ) /\ ( x e. T /\ z e. T ) ) -> ( x = z \/ ( x i^i z ) = (/) ) )
22 13 21 sylan 
 |-  ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( x = z \/ ( x i^i z ) = (/) ) )
23 22 ord 
 |-  ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( -. x = z -> ( x i^i z ) = (/) ) )
24 23 necon1ad 
 |-  ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( ( x i^i z ) =/= (/) -> x = z ) )
25 19 24 syl5 
 |-  ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( ( A e. x /\ A e. z ) -> x = z ) )
26 25 ralrimivva 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A. x e. T A. z e. T ( ( A e. x /\ A e. z ) -> x = z ) )
27 eleq2w 
 |-  ( x = z -> ( A e. x <-> A e. z ) )
28 27 reu4 
 |-  ( E! x e. T A e. x <-> ( E. x e. T A e. x /\ A. x e. T A. z e. T ( ( A e. x /\ A e. z ) -> x = z ) ) )
29 18 26 28 sylanbrc 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> E! x e. T A e. x )