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 ) )