Metamath Proof Explorer

Theorem ustuqtop1

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

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

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 simpl1l 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ ( a e. ( N ` p ) /\ w e. U /\ a = ( w " { p } ) ) ) -> U e. ( UnifOn ` X ) )
3 2 3anassrs 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> U e. ( UnifOn ` X ) )
4 simplr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> w e. U )
5 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U ) -> w C_ ( X X. X ) )
6 3 4 5 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> w C_ ( X X. X ) )
7 simpl1r 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ ( a e. ( N ` p ) /\ w e. U /\ a = ( w " { p } ) ) ) -> p e. X )
8 7 3anassrs 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> p e. X )
9 8 snssd 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> { p } C_ X )
10 simpl3 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ ( a e. ( N ` p ) /\ w e. U /\ a = ( w " { p } ) ) ) -> b C_ X )
11 10 3anassrs 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> b C_ X )
12 xpss12 
 |-  ( ( { p } C_ X /\ b C_ X ) -> ( { p } X. b ) C_ ( X X. X ) )
13 9 11 12 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( { p } X. b ) C_ ( X X. X ) )
14 6 13 unssd 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( w u. ( { p } X. b ) ) C_ ( X X. X ) )
15 ssun1 
 |-  w C_ ( w u. ( { p } X. b ) )
16 15 a1i 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> w C_ ( w u. ( { p } X. b ) ) )
17 ustssel 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U /\ ( w u. ( { p } X. b ) ) C_ ( X X. X ) ) -> ( w C_ ( w u. ( { p } X. b ) ) -> ( w u. ( { p } X. b ) ) e. U ) )
18 17 imp 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ w e. U /\ ( w u. ( { p } X. b ) ) C_ ( X X. X ) ) /\ w C_ ( w u. ( { p } X. b ) ) ) -> ( w u. ( { p } X. b ) ) e. U )
19 3 4 14 16 18 syl31anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( w u. ( { p } X. b ) ) e. U )
20 simpl2 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ ( a e. ( N ` p ) /\ w e. U /\ a = ( w " { p } ) ) ) -> a C_ b )
21 20 3anassrs 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> a C_ b )
22 ssequn1 
 |-  ( a C_ b <-> ( a u. b ) = b )
23 22 biimpi 
 |-  ( a C_ b -> ( a u. b ) = b )
24 id 
 |-  ( a = ( w " { p } ) -> a = ( w " { p } ) )
25 inidm 
 |-  ( { p } i^i { p } ) = { p }
26 vex 
 |-  p e. _V
27 26 snnz 
 |-  { p } =/= (/)
28 25 27 eqnetri 
 |-  ( { p } i^i { p } ) =/= (/)
29 xpima2 
 |-  ( ( { p } i^i { p } ) =/= (/) -> ( ( { p } X. b ) " { p } ) = b )
30 28 29 mp1i 
 |-  ( a = ( w " { p } ) -> ( ( { p } X. b ) " { p } ) = b )
31 30 eqcomd 
 |-  ( a = ( w " { p } ) -> b = ( ( { p } X. b ) " { p } ) )
32 24 31 uneq12d 
 |-  ( a = ( w " { p } ) -> ( a u. b ) = ( ( w " { p } ) u. ( ( { p } X. b ) " { p } ) ) )
33 imaundir 
 |-  ( ( w u. ( { p } X. b ) ) " { p } ) = ( ( w " { p } ) u. ( ( { p } X. b ) " { p } ) )
34 32 33 eqtr4di 
 |-  ( a = ( w " { p } ) -> ( a u. b ) = ( ( w u. ( { p } X. b ) ) " { p } ) )
35 23 34 sylan9req 
 |-  ( ( a C_ b /\ a = ( w " { p } ) ) -> b = ( ( w u. ( { p } X. b ) ) " { p } ) )
36 21 35 sylancom 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> b = ( ( w u. ( { p } X. b ) ) " { p } ) )
37 imaeq1 
 |-  ( u = ( w u. ( { p } X. b ) ) -> ( u " { p } ) = ( ( w u. ( { p } X. b ) ) " { p } ) )
38 37 rspceeqv 
 |-  ( ( ( w u. ( { p } X. b ) ) e. U /\ b = ( ( w u. ( { p } X. b ) ) " { p } ) ) -> E. u e. U b = ( u " { p } ) )
39 19 36 38 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. u e. U b = ( u " { p } ) )
40 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. _V ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
41 40 elvd 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
42 41 biimpa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
43 42 3ad2antl1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
44 39 43 r19.29a 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> E. u e. U b = ( u " { p } ) )
45 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b e. _V ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) )
46 45 elvd 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) )
47 46 3ad2ant1 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) )
48 47 adantr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) )
49 44 48 mpbird 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )