Metamath Proof Explorer

Theorem ustuqtop3

Description: Lemma for ustuqtop , similar to elnei . (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypothesis utopustuq.1 
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
Assertion ustuqtop3 
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 fnresi 
 |-  ( _I |` X ) Fn X
3 fnsnfv 
 |-  ( ( ( _I |` X ) Fn X /\ p e. X ) -> { ( ( _I |` X ) ` p ) } = ( ( _I |` X ) " { p } ) )
4 2 3 mpan 
 |-  ( p e. X -> { ( ( _I |` X ) ` p ) } = ( ( _I |` X ) " { p } ) )
5 4 ad4antlr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> { ( ( _I |` X ) ` p ) } = ( ( _I |` X ) " { p } ) )
6 ustdiag 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U ) -> ( _I |` X ) C_ w )
7 6 ad5ant14 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( _I |` X ) C_ w )
8 imass1 
 |-  ( ( _I |` X ) C_ w -> ( ( _I |` X ) " { p } ) C_ ( w " { p } ) )
9 7 8 syl 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( ( _I |` X ) " { p } ) C_ ( w " { p } ) )
10 5 9 eqsstrd 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> { ( ( _I |` X ) ` p ) } C_ ( w " { p } ) )
11 fvex 
 |-  ( ( _I |` X ) ` p ) e. _V
12 11 snss 
 |-  ( ( ( _I |` X ) ` p ) e. ( w " { p } ) <-> { ( ( _I |` X ) ` p ) } C_ ( w " { p } ) )
13 10 12 sylibr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( ( _I |` X ) ` p ) e. ( w " { p } ) )
14 fvresi 
 |-  ( p e. X -> ( ( _I |` X ) ` p ) = p )
15 14 eqcomd 
 |-  ( p e. X -> p = ( ( _I |` X ) ` p ) )
16 15 ad4antlr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> p = ( ( _I |` X ) ` p ) )
17 simpr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> a = ( w " { p } ) )
18 13 16 17 3eltr4d 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> p e. a )
19 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. _V ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
20 19 elvd 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
21 20 biimpa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
22 18 21 r19.29a 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )