Metamath Proof Explorer


Theorem trust

Description: The trace of a uniform structure U on a subset A is a uniform structure on A . Definition 3 of BourbakiTop1 p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017)

Ref Expression
Assertion trust
|- ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )

Proof

Step Hyp Ref Expression
1 restsspw
 |-  ( U |`t ( A X. A ) ) C_ ~P ( A X. A )
2 1 a1i
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) C_ ~P ( A X. A ) )
3 inxp
 |-  ( ( X X. X ) i^i ( A X. A ) ) = ( ( X i^i A ) X. ( X i^i A ) )
4 sseqin2
 |-  ( A C_ X <-> ( X i^i A ) = A )
5 4 biimpi
 |-  ( A C_ X -> ( X i^i A ) = A )
6 5 sqxpeqd
 |-  ( A C_ X -> ( ( X i^i A ) X. ( X i^i A ) ) = ( A X. A ) )
7 3 6 syl5eq
 |-  ( A C_ X -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
8 7 adantl
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
9 simpl
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> U e. ( UnifOn ` X ) )
10 elfvex
 |-  ( U e. ( UnifOn ` X ) -> X e. _V )
11 10 adantr
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> X e. _V )
12 simpr
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> A C_ X )
13 11 12 ssexd
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> A e. _V )
14 13 13 xpexd
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
15 ustbasel
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) e. U )
16 15 adantr
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( X X. X ) e. U )
17 elrestr
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V /\ ( X X. X ) e. U ) -> ( ( X X. X ) i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) )
18 9 14 16 17 syl3anc
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( ( X X. X ) i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) )
19 8 18 eqeltrrd
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. ( U |`t ( A X. A ) ) )
20 9 ad5antr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> U e. ( UnifOn ` X ) )
21 14 ad5antr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( A X. A ) e. _V )
22 simplr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> u e. U )
23 simp-4r
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> w e. ~P ( A X. A ) )
24 23 elpwid
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> w C_ ( A X. A ) )
25 12 ad5antr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> A C_ X )
26 xpss12
 |-  ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
27 25 25 26 syl2anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( A X. A ) C_ ( X X. X ) )
28 24 27 sstrd
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> w C_ ( X X. X ) )
29 ustssxp
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> u C_ ( X X. X ) )
30 20 22 29 syl2anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> u C_ ( X X. X ) )
31 28 30 unssd
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( w u. u ) C_ ( X X. X ) )
32 ssun2
 |-  u C_ ( w u. u )
33 ustssel
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U /\ ( w u. u ) C_ ( X X. X ) ) -> ( u C_ ( w u. u ) -> ( w u. u ) e. U ) )
34 32 33 mpi
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U /\ ( w u. u ) C_ ( X X. X ) ) -> ( w u. u ) e. U )
35 20 22 31 34 syl3anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( w u. u ) e. U )
36 df-ss
 |-  ( w C_ ( A X. A ) <-> ( w i^i ( A X. A ) ) = w )
37 24 36 sylib
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( w i^i ( A X. A ) ) = w )
38 37 uneq1d
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( ( w i^i ( A X. A ) ) u. ( u i^i ( A X. A ) ) ) = ( w u. ( u i^i ( A X. A ) ) ) )
39 simpr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> v = ( u i^i ( A X. A ) ) )
40 simpllr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> v C_ w )
41 39 40 eqsstrrd
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( u i^i ( A X. A ) ) C_ w )
42 ssequn2
 |-  ( ( u i^i ( A X. A ) ) C_ w <-> ( w u. ( u i^i ( A X. A ) ) ) = w )
43 41 42 sylib
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( w u. ( u i^i ( A X. A ) ) ) = w )
44 38 43 eqtr2d
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> w = ( ( w i^i ( A X. A ) ) u. ( u i^i ( A X. A ) ) ) )
45 indir
 |-  ( ( w u. u ) i^i ( A X. A ) ) = ( ( w i^i ( A X. A ) ) u. ( u i^i ( A X. A ) ) )
46 44 45 eqtr4di
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> w = ( ( w u. u ) i^i ( A X. A ) ) )
47 ineq1
 |-  ( x = ( w u. u ) -> ( x i^i ( A X. A ) ) = ( ( w u. u ) i^i ( A X. A ) ) )
48 47 rspceeqv
 |-  ( ( ( w u. u ) e. U /\ w = ( ( w u. u ) i^i ( A X. A ) ) ) -> E. x e. U w = ( x i^i ( A X. A ) ) )
49 35 46 48 syl2anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> E. x e. U w = ( x i^i ( A X. A ) ) )
50 elrest
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) -> ( w e. ( U |`t ( A X. A ) ) <-> E. x e. U w = ( x i^i ( A X. A ) ) ) )
51 50 biimpar
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) /\ E. x e. U w = ( x i^i ( A X. A ) ) ) -> w e. ( U |`t ( A X. A ) ) )
52 20 21 49 51 syl21anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> w e. ( U |`t ( A X. A ) ) )
53 elrest
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) -> ( v e. ( U |`t ( A X. A ) ) <-> E. u e. U v = ( u i^i ( A X. A ) ) ) )
54 53 biimpa
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) /\ v e. ( U |`t ( A X. A ) ) ) -> E. u e. U v = ( u i^i ( A X. A ) ) )
55 14 54 syldanl
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> E. u e. U v = ( u i^i ( A X. A ) ) )
56 55 ad2antrr
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) -> E. u e. U v = ( u i^i ( A X. A ) ) )
57 52 56 r19.29a
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) /\ v C_ w ) -> w e. ( U |`t ( A X. A ) ) )
58 57 ex
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ~P ( A X. A ) ) -> ( v C_ w -> w e. ( U |`t ( A X. A ) ) ) )
59 58 ralrimiva
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> A. w e. ~P ( A X. A ) ( v C_ w -> w e. ( U |`t ( A X. A ) ) ) )
60 9 ad5antr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> U e. ( UnifOn ` X ) )
61 14 ad5antr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> ( A X. A ) e. _V )
62 simpllr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> u e. U )
63 simplr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> x e. U )
64 ustincl
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U /\ x e. U ) -> ( u i^i x ) e. U )
65 60 62 63 64 syl3anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> ( u i^i x ) e. U )
66 simprl
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> v = ( u i^i ( A X. A ) ) )
67 simprr
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> w = ( x i^i ( A X. A ) ) )
68 66 67 ineq12d
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> ( v i^i w ) = ( ( u i^i ( A X. A ) ) i^i ( x i^i ( A X. A ) ) ) )
69 inindir
 |-  ( ( u i^i x ) i^i ( A X. A ) ) = ( ( u i^i ( A X. A ) ) i^i ( x i^i ( A X. A ) ) )
70 68 69 eqtr4di
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> ( v i^i w ) = ( ( u i^i x ) i^i ( A X. A ) ) )
71 ineq1
 |-  ( y = ( u i^i x ) -> ( y i^i ( A X. A ) ) = ( ( u i^i x ) i^i ( A X. A ) ) )
72 71 rspceeqv
 |-  ( ( ( u i^i x ) e. U /\ ( v i^i w ) = ( ( u i^i x ) i^i ( A X. A ) ) ) -> E. y e. U ( v i^i w ) = ( y i^i ( A X. A ) ) )
73 65 70 72 syl2anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> E. y e. U ( v i^i w ) = ( y i^i ( A X. A ) ) )
74 elrest
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) -> ( ( v i^i w ) e. ( U |`t ( A X. A ) ) <-> E. y e. U ( v i^i w ) = ( y i^i ( A X. A ) ) ) )
75 74 biimpar
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) /\ E. y e. U ( v i^i w ) = ( y i^i ( A X. A ) ) ) -> ( v i^i w ) e. ( U |`t ( A X. A ) ) )
76 60 61 73 75 syl21anc
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ x e. U ) /\ ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) ) -> ( v i^i w ) e. ( U |`t ( A X. A ) ) )
77 55 adantr
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) -> E. u e. U v = ( u i^i ( A X. A ) ) )
78 9 ad2antrr
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) -> U e. ( UnifOn ` X ) )
79 14 ad2antrr
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) -> ( A X. A ) e. _V )
80 simpr
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) -> w e. ( U |`t ( A X. A ) ) )
81 50 biimpa
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) /\ w e. ( U |`t ( A X. A ) ) ) -> E. x e. U w = ( x i^i ( A X. A ) ) )
82 78 79 80 81 syl21anc
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) -> E. x e. U w = ( x i^i ( A X. A ) ) )
83 reeanv
 |-  ( E. u e. U E. x e. U ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) <-> ( E. u e. U v = ( u i^i ( A X. A ) ) /\ E. x e. U w = ( x i^i ( A X. A ) ) ) )
84 77 82 83 sylanbrc
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) -> E. u e. U E. x e. U ( v = ( u i^i ( A X. A ) ) /\ w = ( x i^i ( A X. A ) ) ) )
85 76 84 r19.29vva
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ w e. ( U |`t ( A X. A ) ) ) -> ( v i^i w ) e. ( U |`t ( A X. A ) ) )
86 85 ralrimiva
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> A. w e. ( U |`t ( A X. A ) ) ( v i^i w ) e. ( U |`t ( A X. A ) ) )
87 simp-4l
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> U e. ( UnifOn ` X ) )
88 simplr
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> u e. U )
89 ustdiag
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> ( _I |` X ) C_ u )
90 87 88 89 syl2anc
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( _I |` X ) C_ u )
91 simp-4r
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> A C_ X )
92 inss1
 |-  ( ( _I |` X ) i^i ( A X. A ) ) C_ ( _I |` X )
93 resss
 |-  ( _I |` X ) C_ _I
94 92 93 sstri
 |-  ( ( _I |` X ) i^i ( A X. A ) ) C_ _I
95 iss
 |-  ( ( ( _I |` X ) i^i ( A X. A ) ) C_ _I <-> ( ( _I |` X ) i^i ( A X. A ) ) = ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) ) )
96 94 95 mpbi
 |-  ( ( _I |` X ) i^i ( A X. A ) ) = ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) )
97 simpr
 |-  ( ( A C_ X /\ u e. A ) -> u e. A )
98 ssel2
 |-  ( ( A C_ X /\ u e. A ) -> u e. X )
99 equid
 |-  u = u
100 resieq
 |-  ( ( u e. X /\ u e. X ) -> ( u ( _I |` X ) u <-> u = u ) )
101 99 100 mpbiri
 |-  ( ( u e. X /\ u e. X ) -> u ( _I |` X ) u )
102 98 98 101 syl2anc
 |-  ( ( A C_ X /\ u e. A ) -> u ( _I |` X ) u )
103 breq2
 |-  ( v = u -> ( u ( _I |` X ) v <-> u ( _I |` X ) u ) )
104 103 rspcev
 |-  ( ( u e. A /\ u ( _I |` X ) u ) -> E. v e. A u ( _I |` X ) v )
105 97 102 104 syl2anc
 |-  ( ( A C_ X /\ u e. A ) -> E. v e. A u ( _I |` X ) v )
106 105 ralrimiva
 |-  ( A C_ X -> A. u e. A E. v e. A u ( _I |` X ) v )
107 dminxp
 |-  ( dom ( ( _I |` X ) i^i ( A X. A ) ) = A <-> A. u e. A E. v e. A u ( _I |` X ) v )
108 106 107 sylibr
 |-  ( A C_ X -> dom ( ( _I |` X ) i^i ( A X. A ) ) = A )
109 108 reseq2d
 |-  ( A C_ X -> ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) ) = ( _I |` A ) )
110 96 109 eqtr2id
 |-  ( A C_ X -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
111 110 adantl
 |-  ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
112 ssrin
 |-  ( ( _I |` X ) C_ u -> ( ( _I |` X ) i^i ( A X. A ) ) C_ ( u i^i ( A X. A ) ) )
113 112 adantr
 |-  ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( ( _I |` X ) i^i ( A X. A ) ) C_ ( u i^i ( A X. A ) ) )
114 111 113 eqsstrd
 |-  ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) C_ ( u i^i ( A X. A ) ) )
115 90 91 114 syl2anc
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( _I |` A ) C_ ( u i^i ( A X. A ) ) )
116 simpr
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> v = ( u i^i ( A X. A ) ) )
117 115 116 sseqtrrd
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( _I |` A ) C_ v )
118 117 55 r19.29a
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> ( _I |` A ) C_ v )
119 14 ad3antrrr
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( A X. A ) e. _V )
120 ustinvel
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> `' u e. U )
121 87 88 120 syl2anc
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> `' u e. U )
122 116 cnveqd
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> `' v = `' ( u i^i ( A X. A ) ) )
123 cnvin
 |-  `' ( u i^i ( A X. A ) ) = ( `' u i^i `' ( A X. A ) )
124 cnvxp
 |-  `' ( A X. A ) = ( A X. A )
125 124 ineq2i
 |-  ( `' u i^i `' ( A X. A ) ) = ( `' u i^i ( A X. A ) )
126 123 125 eqtri
 |-  `' ( u i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) )
127 122 126 eqtrdi
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> `' v = ( `' u i^i ( A X. A ) ) )
128 ineq1
 |-  ( x = `' u -> ( x i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) ) )
129 128 rspceeqv
 |-  ( ( `' u e. U /\ `' v = ( `' u i^i ( A X. A ) ) ) -> E. x e. U `' v = ( x i^i ( A X. A ) ) )
130 121 127 129 syl2anc
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> E. x e. U `' v = ( x i^i ( A X. A ) ) )
131 elrest
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) -> ( `' v e. ( U |`t ( A X. A ) ) <-> E. x e. U `' v = ( x i^i ( A X. A ) ) ) )
132 131 biimpar
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) /\ E. x e. U `' v = ( x i^i ( A X. A ) ) ) -> `' v e. ( U |`t ( A X. A ) ) )
133 87 119 130 132 syl21anc
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> `' v e. ( U |`t ( A X. A ) ) )
134 133 55 r19.29a
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> `' v e. ( U |`t ( A X. A ) ) )
135 simp-4l
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> U e. ( UnifOn ` X ) )
136 14 ad3antrrr
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> ( A X. A ) e. _V )
137 simplr
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> x e. U )
138 elrestr
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V /\ x e. U ) -> ( x i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) )
139 135 136 137 138 syl3anc
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> ( x i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) )
140 inss1
 |-  ( x i^i ( A X. A ) ) C_ x
141 coss1
 |-  ( ( x i^i ( A X. A ) ) C_ x -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( x o. ( x i^i ( A X. A ) ) ) )
142 coss2
 |-  ( ( x i^i ( A X. A ) ) C_ x -> ( x o. ( x i^i ( A X. A ) ) ) C_ ( x o. x ) )
143 141 142 sstrd
 |-  ( ( x i^i ( A X. A ) ) C_ x -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( x o. x ) )
144 140 143 ax-mp
 |-  ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( x o. x )
145 sstr
 |-  ( ( ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( x o. x ) /\ ( x o. x ) C_ u ) -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ u )
146 144 145 mpan
 |-  ( ( x o. x ) C_ u -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ u )
147 146 adantl
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ u )
148 inss2
 |-  ( x i^i ( A X. A ) ) C_ ( A X. A )
149 coss1
 |-  ( ( x i^i ( A X. A ) ) C_ ( A X. A ) -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( ( A X. A ) o. ( x i^i ( A X. A ) ) ) )
150 coss2
 |-  ( ( x i^i ( A X. A ) ) C_ ( A X. A ) -> ( ( A X. A ) o. ( x i^i ( A X. A ) ) ) C_ ( ( A X. A ) o. ( A X. A ) ) )
151 149 150 sstrd
 |-  ( ( x i^i ( A X. A ) ) C_ ( A X. A ) -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( ( A X. A ) o. ( A X. A ) ) )
152 148 151 ax-mp
 |-  ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( ( A X. A ) o. ( A X. A ) )
153 xpidtr
 |-  ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
154 152 153 sstri
 |-  ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( A X. A )
155 154 a1i
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( A X. A ) )
156 147 155 ssind
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( u i^i ( A X. A ) ) )
157 id
 |-  ( w = ( x i^i ( A X. A ) ) -> w = ( x i^i ( A X. A ) ) )
158 157 157 coeq12d
 |-  ( w = ( x i^i ( A X. A ) ) -> ( w o. w ) = ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) )
159 158 sseq1d
 |-  ( w = ( x i^i ( A X. A ) ) -> ( ( w o. w ) C_ ( u i^i ( A X. A ) ) <-> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( u i^i ( A X. A ) ) ) )
160 159 rspcev
 |-  ( ( ( x i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) /\ ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( u i^i ( A X. A ) ) ) -> E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ ( u i^i ( A X. A ) ) )
161 139 156 160 syl2anc
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ ( u i^i ( A X. A ) ) )
162 ustexhalf
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> E. x e. U ( x o. x ) C_ u )
163 162 adantlr
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) -> E. x e. U ( x o. x ) C_ u )
164 161 163 r19.29a
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ u e. U ) -> E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ ( u i^i ( A X. A ) ) )
165 164 ad4ant13
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ ( u i^i ( A X. A ) ) )
166 116 sseq2d
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( ( w o. w ) C_ v <-> ( w o. w ) C_ ( u i^i ( A X. A ) ) ) )
167 166 rexbidv
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> ( E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v <-> E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ ( u i^i ( A X. A ) ) ) )
168 165 167 mpbird
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) /\ u e. U ) /\ v = ( u i^i ( A X. A ) ) ) -> E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v )
169 168 55 r19.29a
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v )
170 118 134 169 3jca
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> ( ( _I |` A ) C_ v /\ `' v e. ( U |`t ( A X. A ) ) /\ E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v ) )
171 59 86 170 3jca
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X ) /\ v e. ( U |`t ( A X. A ) ) ) -> ( A. w e. ~P ( A X. A ) ( v C_ w -> w e. ( U |`t ( A X. A ) ) ) /\ A. w e. ( U |`t ( A X. A ) ) ( v i^i w ) e. ( U |`t ( A X. A ) ) /\ ( ( _I |` A ) C_ v /\ `' v e. ( U |`t ( A X. A ) ) /\ E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v ) ) )
172 171 ralrimiva
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> A. v e. ( U |`t ( A X. A ) ) ( A. w e. ~P ( A X. A ) ( v C_ w -> w e. ( U |`t ( A X. A ) ) ) /\ A. w e. ( U |`t ( A X. A ) ) ( v i^i w ) e. ( U |`t ( A X. A ) ) /\ ( ( _I |` A ) C_ v /\ `' v e. ( U |`t ( A X. A ) ) /\ E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v ) ) )
173 2 19 172 3jca
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( ( U |`t ( A X. A ) ) C_ ~P ( A X. A ) /\ ( A X. A ) e. ( U |`t ( A X. A ) ) /\ A. v e. ( U |`t ( A X. A ) ) ( A. w e. ~P ( A X. A ) ( v C_ w -> w e. ( U |`t ( A X. A ) ) ) /\ A. w e. ( U |`t ( A X. A ) ) ( v i^i w ) e. ( U |`t ( A X. A ) ) /\ ( ( _I |` A ) C_ v /\ `' v e. ( U |`t ( A X. A ) ) /\ E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v ) ) ) )
174 isust
 |-  ( A e. _V -> ( ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) <-> ( ( U |`t ( A X. A ) ) C_ ~P ( A X. A ) /\ ( A X. A ) e. ( U |`t ( A X. A ) ) /\ A. v e. ( U |`t ( A X. A ) ) ( A. w e. ~P ( A X. A ) ( v C_ w -> w e. ( U |`t ( A X. A ) ) ) /\ A. w e. ( U |`t ( A X. A ) ) ( v i^i w ) e. ( U |`t ( A X. A ) ) /\ ( ( _I |` A ) C_ v /\ `' v e. ( U |`t ( A X. A ) ) /\ E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v ) ) ) ) )
175 13 174 syl
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) <-> ( ( U |`t ( A X. A ) ) C_ ~P ( A X. A ) /\ ( A X. A ) e. ( U |`t ( A X. A ) ) /\ A. v e. ( U |`t ( A X. A ) ) ( A. w e. ~P ( A X. A ) ( v C_ w -> w e. ( U |`t ( A X. A ) ) ) /\ A. w e. ( U |`t ( A X. A ) ) ( v i^i w ) e. ( U |`t ( A X. A ) ) /\ ( ( _I |` A ) C_ v /\ `' v e. ( U |`t ( A X. A ) ) /\ E. w e. ( U |`t ( A X. A ) ) ( w o. w ) C_ v ) ) ) ) )
176 173 175 mpbird
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )