Metamath Proof Explorer

Theorem ustuqtop2

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 ustuqtop2 
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 simp-6l 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( U e. ( UnifOn ` X ) /\ p e. X ) )
3 simp-7l 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> U e. ( UnifOn ` X ) )
4 simp-4r 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> w e. U )
5 simplr 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> u e. U )
6 ustincl 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U /\ u e. U ) -> ( w i^i u ) e. U )
7 3 4 5 6 syl3anc 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( w i^i u ) e. U )
8 ineq12 
 |-  ( ( a = ( w " { p } ) /\ b = ( u " { p } ) ) -> ( a i^i b ) = ( ( w " { p } ) i^i ( u " { p } ) ) )
9 inimasn 
 |-  ( p e. _V -> ( ( w i^i u ) " { p } ) = ( ( w " { p } ) i^i ( u " { p } ) ) )
10 9 elv 
 |-  ( ( w i^i u ) " { p } ) = ( ( w " { p } ) i^i ( u " { p } ) )
11 8 10 eqtr4di 
 |-  ( ( a = ( w " { p } ) /\ b = ( u " { p } ) ) -> ( a i^i b ) = ( ( w i^i u ) " { p } ) )
12 11 ad4ant24 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( a i^i b ) = ( ( w i^i u ) " { p } ) )
13 imaeq1 
 |-  ( x = ( w i^i u ) -> ( x " { p } ) = ( ( w i^i u ) " { p } ) )
14 13 rspceeqv 
 |-  ( ( ( w i^i u ) e. U /\ ( a i^i b ) = ( ( w i^i u ) " { p } ) ) -> E. x e. U ( a i^i b ) = ( x " { p } ) )
15 7 12 14 syl2anc 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> E. x e. U ( a i^i b ) = ( x " { p } ) )
16 vex 
 |-  a e. _V
17 16 inex1 
 |-  ( a i^i b ) e. _V
18 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( a i^i b ) e. _V ) -> ( ( a i^i b ) e. ( N ` p ) <-> E. x e. U ( a i^i b ) = ( x " { p } ) ) )
19 17 18 mpan2 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( ( a i^i b ) e. ( N ` p ) <-> E. x e. U ( a i^i b ) = ( x " { p } ) ) )
20 19 biimpar 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ E. x e. U ( a i^i b ) = ( x " { p } ) ) -> ( a i^i b ) e. ( N ` p ) )
21 2 15 20 syl2anc 
 |-  ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( a i^i b ) e. ( N ` p ) )
22 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b e. _V ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) )
23 22 elvd 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) )
24 23 biimpa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b e. ( N ` p ) ) -> E. u e. U b = ( u " { p } ) )
25 24 ad5ant13 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. u e. U b = ( u " { p } ) )
26 21 25 r19.29a 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( a i^i b ) e. ( N ` p ) )
27 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. _V ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
28 27 elvd 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
29 28 biimpa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
30 29 adantr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
31 26 30 r19.29a 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) -> ( a i^i b ) e. ( N ` p ) )
32 31 ralrimiva 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) )
33 32 ralrimiva 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> A. a e. ( N ` p ) A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) )
34 fvex 
 |-  ( N ` p ) e. _V
35 inficl 
 |-  ( ( N ` p ) e. _V -> ( A. a e. ( N ` p ) A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) <-> ( fi ` ( N ` p ) ) = ( N ` p ) ) )
36 34 35 ax-mp 
 |-  ( A. a e. ( N ` p ) A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) <-> ( fi ` ( N ` p ) ) = ( N ` p ) )
37 33 36 sylib 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) = ( N ` p ) )
38 eqimss 
 |-  ( ( fi ` ( N ` p ) ) = ( N ` p ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
39 37 38 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )