Metamath Proof Explorer

Theorem ustuqtop5

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

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

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 ustbasel 
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) e. U )
3 snssi 
 |-  ( p e. X -> { p } C_ X )
4 dfss 
 |-  ( { p } C_ X <-> { p } = ( { p } i^i X ) )
5 3 4 sylib 
 |-  ( p e. X -> { p } = ( { p } i^i X ) )
6 incom 
 |-  ( { p } i^i X ) = ( X i^i { p } )
7 5 6 eqtr2di 
 |-  ( p e. X -> ( X i^i { p } ) = { p } )
8 snnzg 
 |-  ( p e. X -> { p } =/= (/) )
9 7 8 eqnetrd 
 |-  ( p e. X -> ( X i^i { p } ) =/= (/) )
10 9 adantl 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( X i^i { p } ) =/= (/) )
11 xpima2 
 |-  ( ( X i^i { p } ) =/= (/) -> ( ( X X. X ) " { p } ) = X )
12 10 11 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( ( X X. X ) " { p } ) = X )
13 12 eqcomd 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> X = ( ( X X. X ) " { p } ) )
14 imaeq1 
 |-  ( w = ( X X. X ) -> ( w " { p } ) = ( ( X X. X ) " { p } ) )
15 14 rspceeqv 
 |-  ( ( ( X X. X ) e. U /\ X = ( ( X X. X ) " { p } ) ) -> E. w e. U X = ( w " { p } ) )
16 2 13 15 syl2an2r 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> E. w e. U X = ( w " { p } ) )
17 elfvex 
 |-  ( U e. ( UnifOn ` X ) -> X e. _V )
18 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ X e. _V ) -> ( X e. ( N ` p ) <-> E. w e. U X = ( w " { p } ) ) )
19 17 18 mpidan 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( X e. ( N ` p ) <-> E. w e. U X = ( w " { p } ) ) )
20 16 19 mpbird 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> X e. ( N ` p ) )