Metamath Proof Explorer

Theorem cvmsiota

Description: Identify the unique element of T containing A . (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
cvmsiota.2 
|- W = ( iota_ x e. T A e. x )
Assertion cvmsiota 
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> ( W e. T /\ A e. W ) )

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 cvmsiota.2 
 |-  W = ( iota_ x e. T A e. x )
4 1 2 cvmseu 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> E! x e. T A e. x )
5 riotacl2 
 |-  ( E! x e. T A e. x -> ( iota_ x e. T A e. x ) e. { x e. T | A e. x } )
6 4 5 syl 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> ( iota_ x e. T A e. x ) e. { x e. T | A e. x } )
7 3 6 eqeltrid 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> W e. { x e. T | A e. x } )
8 eleq2 
 |-  ( v = W -> ( A e. v <-> A e. W ) )
9 eleq2 
 |-  ( x = v -> ( A e. x <-> A e. v ) )
10 9 cbvrabv 
 |-  { x e. T | A e. x } = { v e. T | A e. v }
11 8 10 elrab2 
 |-  ( W e. { x e. T | A e. x } <-> ( W e. T /\ A e. W ) )
12 7 11 sylib 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> ( W e. T /\ A e. W ) )