Metamath Proof Explorer

Theorem ustuqtop0

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 ustuqtop0 
|- ( U e. ( UnifOn ` X ) -> N : X --> ~P ~P X )

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 ustimasn 
 |-  ( ( U e. ( UnifOn ` X ) /\ v e. U /\ p e. X ) -> ( v " { p } ) C_ X )
3 2 3expa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ v e. U ) /\ p e. X ) -> ( v " { p } ) C_ X )
4 3 an32s 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ v e. U ) -> ( v " { p } ) C_ X )
5 vex 
 |-  v e. _V
6 5 imaex 
 |-  ( v " { p } ) e. _V
7 6 elpw 
 |-  ( ( v " { p } ) e. ~P X <-> ( v " { p } ) C_ X )
8 4 7 sylibr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ v e. U ) -> ( v " { p } ) e. ~P X )
9 8 ralrimiva 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> A. v e. U ( v " { p } ) e. ~P X )
10 eqid 
 |-  ( v e. U |-> ( v " { p } ) ) = ( v e. U |-> ( v " { p } ) )
11 10 rnmptss 
 |-  ( A. v e. U ( v " { p } ) e. ~P X -> ran ( v e. U |-> ( v " { p } ) ) C_ ~P X )
12 9 11 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ran ( v e. U |-> ( v " { p } ) ) C_ ~P X )
13 mptexg 
 |-  ( U e. ( UnifOn ` X ) -> ( v e. U |-> ( v " { p } ) ) e. _V )
14 rnexg 
 |-  ( ( v e. U |-> ( v " { p } ) ) e. _V -> ran ( v e. U |-> ( v " { p } ) ) e. _V )
15 elpwg 
 |-  ( ran ( v e. U |-> ( v " { p } ) ) e. _V -> ( ran ( v e. U |-> ( v " { p } ) ) e. ~P ~P X <-> ran ( v e. U |-> ( v " { p } ) ) C_ ~P X ) )
16 13 14 15 3syl 
 |-  ( U e. ( UnifOn ` X ) -> ( ran ( v e. U |-> ( v " { p } ) ) e. ~P ~P X <-> ran ( v e. U |-> ( v " { p } ) ) C_ ~P X ) )
17 16 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( ran ( v e. U |-> ( v " { p } ) ) e. ~P ~P X <-> ran ( v e. U |-> ( v " { p } ) ) C_ ~P X ) )
18 12 17 mpbird 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ran ( v e. U |-> ( v " { p } ) ) e. ~P ~P X )
19 18 1 fmptd 
 |-  ( U e. ( UnifOn ` X ) -> N : X --> ~P ~P X )