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