This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ustuqtoplem

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 ustuqtoplem 
|- ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ A e. V ) -> ( A e. ( N ` P ) <-> E. w e. U A = ( w " { P } ) ) )

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 simpl 
 |-  ( ( p = q /\ v e. U ) -> p = q )
3 2 sneqd 
 |-  ( ( p = q /\ v e. U ) -> { p } = { q } )
4 3 imaeq2d 
 |-  ( ( p = q /\ v e. U ) -> ( v " { p } ) = ( v " { q } ) )
5 4 mpteq2dva 
 |-  ( p = q -> ( v e. U |-> ( v " { p } ) ) = ( v e. U |-> ( v " { q } ) ) )
6 5 rneqd 
 |-  ( p = q -> ran ( v e. U |-> ( v " { p } ) ) = ran ( v e. U |-> ( v " { q } ) ) )
7 6 cbvmptv 
 |-  ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) ) = ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) )
8 1 7 eqtri 
 |-  N = ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) )
9 simpr2 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( P e. X /\ q = P /\ v e. U ) ) -> q = P )
10 9 sneqd 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( P e. X /\ q = P /\ v e. U ) ) -> { q } = { P } )
11 10 imaeq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( P e. X /\ q = P /\ v e. U ) ) -> ( v " { q } ) = ( v " { P } ) )
12 11 3anassrs 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ q = P ) /\ v e. U ) -> ( v " { q } ) = ( v " { P } ) )
13 12 mpteq2dva 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ q = P ) -> ( v e. U |-> ( v " { q } ) ) = ( v e. U |-> ( v " { P } ) ) )
14 13 rneqd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ q = P ) -> ran ( v e. U |-> ( v " { q } ) ) = ran ( v e. U |-> ( v " { P } ) ) )
15 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> P e. X )
16 mptexg 
 |-  ( U e. ( UnifOn ` X ) -> ( v e. U |-> ( v " { P } ) ) e. _V )
17 rnexg 
 |-  ( ( v e. U |-> ( v " { P } ) ) e. _V -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
18 16 17 syl 
 |-  ( U e. ( UnifOn ` X ) -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
19 18 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
20 8 14 15 19 fvmptd2 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( N ` P ) = ran ( v e. U |-> ( v " { P } ) ) )
21 20 eleq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( A e. ( N ` P ) <-> A e. ran ( v e. U |-> ( v " { P } ) ) ) )
22 imaeq1 
 |-  ( v = w -> ( v " { P } ) = ( w " { P } ) )
23 22 cbvmptv 
 |-  ( v e. U |-> ( v " { P } ) ) = ( w e. U |-> ( w " { P } ) )
24 23 elrnmpt 
 |-  ( A e. V -> ( A e. ran ( v e. U |-> ( v " { P } ) ) <-> E. w e. U A = ( w " { P } ) ) )
25 21 24 sylan9bb 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ A e. V ) -> ( A e. ( N ` P ) <-> E. w e. U A = ( w " { P } ) ) )