Theorem trust 21230

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

Assertion

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

Proof of Theorem trust

Dummy variables v u w x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		restsspw 15317	. . . 4 |- ( U ↾t ( A X. A ) ) C_ ~P ( A X. A )
2	1	a1i 11	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) C_ ~P ( A X. A ) )
3		inxp 4982	. . . . . 6 |- ( ( X X. X ) i^i ( A X. A ) ) = ( ( X i^i A ) X. ( X i^i A ) )
4		dfss1 3667	. . . . . . . 8 |- ( A C_ X <-> ( X i^i A ) = A )
5	4	biimpi 197	. . . . . . 7 |- ( A C_ X -> ( X i^i A ) = A )
6	5	sqxpeqd 4875	. . . . . 6 |- ( A C_ X -> ( ( X i^i A ) X. ( X i^i A ) ) = ( A X. A ) )
7	3, 6	syl5eq 2475	. . . . 5 |- ( A C_ X -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
8	7	adantl 467	. . . 4 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
9		simpl 458	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> U e. (UnifOn ` X ) )
10		elfvex 5904	. . . . . . . 8 |- ( U e. (UnifOn ` X ) -> X e. _V )
11	10	adantr 466	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> X e. _V )
12		simpr 462	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A C_ X )
13	11, 12	ssexd 4567	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
14		xpexg 6603	. . . . . 6 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
15	13, 13, 14	syl2anc 665	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
16		ustbasel 21207	. . . . . 6 |- ( U e. (UnifOn ` X ) -> ( X X. X ) e. U )
17	16	adantr 466	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( X X. X ) e. U )
18		elrestr 15314	. . . . 5 |- ( ( 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 ) ) )
19	9, 15, 17, 18	syl3anc 1264	. . . 4 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( ( X X. X ) i^i ( A X. A ) ) e. ( U ↾t ( A X. A ) ) )
20	8, 19	eqeltrrd 2511	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. ( U ↾t ( A X. A ) ) )
21	9	ad5antr 738	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 ) )
22	15	ad5antr 738	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 )
23		simplr 760	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
24		simp-4r 775	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 ) )
25	24	elpwid 3989	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( 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 ) )
26	12	ad5antr 738	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 )
27		xpss12 4955	. . . . . . . . . . . . . 14 |- ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
28	26, 26, 27	syl2anc 665	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( 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 ) )
29	25, 28	sstrd 3474	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) )
30		ustssxp 21205	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> u C_ ( X X. X ) )
31	21, 23, 30	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) )
32	29, 31	unssd 3642	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) )
33		ssun2 3630	. . . . . . . . . . . 12 |- u C_ ( w u. u )
34		ustssel 21206	. . . . . . . . . . . 12 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ ( w u. u ) C_ ( X X. X ) ) -> ( u C_ ( w u. u ) -> ( w u. u ) e. U ) )
35	33, 34	mpi 21	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ ( w u. u ) C_ ( X X. X ) ) -> ( w u. u ) e. U )
36	21, 23, 32, 35	syl3anc 1264	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 )
37		df-ss 3450	. . . . . . . . . . . . . 14 |- ( w C_ ( A X. A ) <-> ( w i^i ( A X. A ) ) = w )
38	25, 37	sylib 199	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( 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 )
39	38	uneq1d 3619	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) ) ) )
40		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 ) ) )
41		simpllr 767	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 )
42	40, 41	eqsstr3d 3499	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( 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 )
43		ssequn2 3639	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) C_ w <-> ( w u. ( u i^i ( A X. A ) ) ) = w )
44	42, 43	sylib 199	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 )
45	39, 44	eqtr2d 2464	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) ) ) )
46		indir 3721	. . . . . . . . . . 11 |- ( ( w u. u ) i^i ( A X. A ) ) = ( ( w i^i ( A X. A ) ) u. ( u i^i ( A X. A ) ) )
47	45, 46	syl6eqr 2481	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 ) ) )
48		ineq1 3657	. . . . . . . . . . . 12 |- ( x = ( w u. u ) -> ( x i^i ( A X. A ) ) = ( ( w u. u ) i^i ( A X. A ) ) )
49	48	eqeq2d 2436	. . . . . . . . . . 11 |- ( x = ( w u. u ) -> ( w = ( x i^i ( A X. A ) ) <-> w = ( ( w u. u ) i^i ( A X. A ) ) ) )
50	49	rspcev 3182	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
51	36, 47, 50	syl2anc 665	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 ) ) )
52		elrest 15313	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
53	52	biimpar 487	. . . . . . . . 9 |- ( ( ( 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 ) ) )
54	21, 22, 51, 53	syl21anc 1263	. . . . . . . 8 |- ( ( ( ( ( ( ( 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 ) ) )
55		simp1 1005	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> U e. (UnifOn ` X ) )
56	15	3adant3 1025	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> ( A X. A ) e. _V )
57		simp3 1007	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> v e. ( U ↾t ( A X. A ) ) )
58		elrest 15313	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
59	58	biimpa 486	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
60	55, 56, 57, 59	syl21anc 1263	. . . . . . . . . 10 |- ( ( 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 ) ) )
61	60	3expa 1205	. . . . . . . . 9 |- ( ( ( 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 ) ) )
62	61	ad2antrr 730	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
63	54, 62	r19.29a 2970	. . . . . . 7 |- ( ( ( ( ( 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 ) ) )
64	63	ex 435	. . . . . 6 |- ( ( ( ( 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 ) ) ) )
65	64	ralrimiva 2839	. . . . 5 |- ( ( ( 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 ) ) ) )
66	9	ad5antr 738	. . . . . . . 8 |- ( ( ( ( ( ( ( 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 ) )
67	15	ad5antr 738	. . . . . . . 8 |- ( ( ( ( ( ( ( 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 )
68		simpllr 767	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 )
69		simplr 760	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 )
70		ustincl 21208	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ x e. U ) -> ( u i^i x ) e. U )
71	66, 68, 69, 70	syl3anc 1264	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 )
72		simprl 762	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) ) )
73		simprr 764	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) ) )
74	72, 73	ineq12d 3665	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 ) ) ) )
75		inindir 3680	. . . . . . . . . 10 |- ( ( u i^i x ) i^i ( A X. A ) ) = ( ( u i^i ( A X. A ) ) i^i ( x i^i ( A X. A ) ) )
76	74, 75	syl6eqr 2481	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 ) ) )
77		ineq1 3657	. . . . . . . . . . 11 |- ( y = ( u i^i x ) -> ( y i^i ( A X. A ) ) = ( ( u i^i x ) i^i ( A X. A ) ) )
78	77	eqeq2d 2436	. . . . . . . . . 10 |- ( y = ( u i^i x ) -> ( ( v i^i w ) = ( y i^i ( A X. A ) ) <-> ( v i^i w ) = ( ( u i^i x ) i^i ( A X. A ) ) ) )
79	78	rspcev 3182	. . . . . . . . 9 |- ( ( ( 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 ) ) )
80	71, 76, 79	syl2anc 665	. . . . . . . 8 |- ( ( ( ( ( ( ( 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 ) ) )
81		elrest 15313	. . . . . . . . 9 |- ( ( 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 ) ) ) )
82	81	biimpar 487	. . . . . . . 8 |- ( ( ( 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 ) ) )
83	66, 67, 80, 82	syl21anc 1263	. . . . . . 7 |- ( ( ( ( ( ( ( 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 ) ) )
84	61	adantr 466	. . . . . . . 8 |- ( ( ( ( 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 ) ) )
85	9	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ( 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 ) )
86	15	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ( 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 )
87		simpr 462	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
88	52	biimpa 486	. . . . . . . . 9 |- ( ( ( 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 ) ) )
89	85, 86, 87, 88	syl21anc 1263	. . . . . . . 8 |- ( ( ( ( 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 ) ) )
90		reeanv 2996	. . . . . . . 8 |- ( 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 ) ) ) )
91	84, 89, 90	sylanbrc 668	. . . . . . 7 |- ( ( ( ( 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 ) ) ) )
92	83, 91	r19.29vva 2972	. . . . . 6 |- ( ( ( ( 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 ) ) )
93	92	ralrimiva 2839	. . . . 5 |- ( ( ( 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 ) ) )
94		simp-4l 774	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) )
95		simplr 760	. . . . . . . . . 10 |- ( ( ( ( ( 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 )
96		ustdiag 21209	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> ( _I |` X ) C_ u )
97	94, 95, 96	syl2anc 665	. . . . . . . . 9 |- ( ( ( ( ( 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 )
98		simp-4r 775	. . . . . . . . 9 |- ( ( ( ( ( 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 )
99		inss1 3682	. . . . . . . . . . . . . 14 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ ( _I |` X )
100		resss 5143	. . . . . . . . . . . . . 14 |- ( _I |` X ) C_ _I
101	99, 100	sstri 3473	. . . . . . . . . . . . 13 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ _I
102		iss 5167	. . . . . . . . . . . . 13 |- ( ( ( _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 ) ) ) )
103	101, 102	mpbi 211	. . . . . . . . . . . 12 |- ( ( _I |` X ) i^i ( A X. A ) ) = ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) )
104		simpr 462	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u e. A )
105		ssel2 3459	. . . . . . . . . . . . . . . . 17 |- ( ( A C_ X /\ u e. A ) -> u e. X )
106		equid 1840	. . . . . . . . . . . . . . . . . 18 |- u = u
107		resieq 5130	. . . . . . . . . . . . . . . . . 18 |- ( ( u e. X /\ u e. X ) -> ( u ( _I |` X ) u <-> u = u ) )
108	106, 107	mpbiri 236	. . . . . . . . . . . . . . . . 17 |- ( ( u e. X /\ u e. X ) -> u ( _I |` X ) u )
109	105, 105, 108	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u ( _I |` X ) u )
110		breq2 4424	. . . . . . . . . . . . . . . . 17 |- ( v = u -> ( u ( _I |` X ) v <-> u ( _I |` X ) u ) )
111	110	rspcev 3182	. . . . . . . . . . . . . . . 16 |- ( ( u e. A /\ u ( _I |` X ) u ) -> E. v e. A u ( _I |` X ) v )
112	104, 109, 111	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( A C_ X /\ u e. A ) -> E. v e. A u ( _I |` X ) v )
113	112	ralrimiva 2839	. . . . . . . . . . . . . 14 |- ( A C_ X -> A. u e. A E. v e. A u ( _I |` X ) v )
114		dminxp 5292	. . . . . . . . . . . . . 14 |- ( dom ( ( _I |` X ) i^i ( A X. A ) ) = A <-> A. u e. A E. v e. A u ( _I |` X ) v )
115	113, 114	sylibr 215	. . . . . . . . . . . . 13 |- ( A C_ X -> dom ( ( _I |` X ) i^i ( A X. A ) ) = A )
116	115	reseq2d 5120	. . . . . . . . . . . 12 |- ( A C_ X -> ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) ) = ( _I |` A ) )
117	103, 116	syl5req 2476	. . . . . . . . . . 11 |- ( A C_ X -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
118	117	adantl 467	. . . . . . . . . 10 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
119		ssrin 3687	. . . . . . . . . . 11 |- ( ( _I |` X ) C_ u -> ( ( _I |` X ) i^i ( A X. A ) ) C_ ( u i^i ( A X. A ) ) )
120	119	adantr 466	. . . . . . . . . 10 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( ( _I |` X ) i^i ( A X. A ) ) C_ ( u i^i ( A X. A ) ) )
121	118, 120	eqsstrd 3498	. . . . . . . . 9 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) C_ ( u i^i ( A X. A ) ) )
122	97, 98, 121	syl2anc 665	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
123		simpr 462	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
124	122, 123	sseqtr4d 3501	. . . . . . 7 |- ( ( ( ( ( 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 )
125	124, 61	r19.29a 2970	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ v e. ( U ↾t ( A X. A ) ) ) -> ( _I |` A ) C_ v )
126	15	ad3antrrr 734	. . . . . . . 8 |- ( ( ( ( ( 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 )
127		ustinvel 21210	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> `' u e. U )
128	94, 95, 127	syl2anc 665	. . . . . . . . 9 |- ( ( ( ( ( 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 )
129	123	cnveqd 5025	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) )
130		cnvin 5258	. . . . . . . . . . 11 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i `' ( A X. A ) )
131		cnvxp 5269	. . . . . . . . . . . 12 |- `' ( A X. A ) = ( A X. A )
132	131	ineq2i 3661	. . . . . . . . . . 11 |- ( `' u i^i `' ( A X. A ) ) = ( `' u i^i ( A X. A ) )
133	130, 132	eqtri 2451	. . . . . . . . . 10 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) )
134	129, 133	syl6eq 2479	. . . . . . . . 9 |- ( ( ( ( ( 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 ) ) )
135		ineq1 3657	. . . . . . . . . . 11 |- ( x = `' u -> ( x i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) ) )
136	135	eqeq2d 2436	. . . . . . . . . 10 |- ( x = `' u -> ( `' v = ( x i^i ( A X. A ) ) <-> `' v = ( `' u i^i ( A X. A ) ) ) )
137	136	rspcev 3182	. . . . . . . . 9 |- ( ( `' u e. U /\ `' v = ( `' u i^i ( A X. A ) ) ) -> E. x e. U `' v = ( x i^i ( A X. A ) ) )
138	128, 134, 137	syl2anc 665	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
139		elrest 15313	. . . . . . . . 9 |- ( ( 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 ) ) ) )
140	139	biimpar 487	. . . . . . . 8 |- ( ( ( 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 ) ) )
141	94, 126, 138, 140	syl21anc 1263	. . . . . . 7 |- ( ( ( ( ( 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 ) ) )
142	141, 61	r19.29a 2970	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ v e. ( U ↾t ( A X. A ) ) ) -> `' v e. ( U ↾t ( A X. A ) ) )
143		simp-4l 774	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> U e. (UnifOn ` X ) )
144	15	ad3antrrr 734	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> ( A X. A ) e. _V )
145		simplr 760	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> x e. U )
146		elrestr 15314	. . . . . . . . . . . 12 |- ( ( U e. (UnifOn ` X ) /\ ( A X. A ) e. _V /\ x e. U ) -> ( x i^i ( A X. A ) ) e. ( U ↾t ( A X. A ) ) )
147	143, 144, 145, 146	syl3anc 1264	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) )
148		inss1 3682	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ x
149		coss1 5005	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
150		coss2 5006	. . . . . . . . . . . . . . . 16 |- ( ( x i^i ( A X. A ) ) C_ x -> ( x o. ( x i^i ( A X. A ) ) ) C_ ( x o. x ) )
151	149, 150	sstrd 3474	. . . . . . . . . . . . . . 15 |- ( ( 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 ) )
152	148, 151	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( x o. x )
153		sstr 3472	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
154	152, 153	mpan 674	. . . . . . . . . . . . 13 |- ( ( x o. x ) C_ u -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ u )
155	154	adantl 467	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
156		inss2 3683	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ ( A X. A )
157		coss1 5005	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
158		coss2 5006	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
159	157, 158	sstrd 3474	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) )
160	156, 159	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( ( A X. A ) o. ( A X. A ) )
161		xpidtr 5237	. . . . . . . . . . . . . 14 |- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
162	160, 161	sstri 3473	. . . . . . . . . . . . 13 |- ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( A X. A )
163	162	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
164	155, 163	ssind 3686	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) )
165		id 23	. . . . . . . . . . . . . 14 |- ( w = ( x i^i ( A X. A ) ) -> w = ( x i^i ( A X. A ) ) )
166	165, 165	coeq12d 5014	. . . . . . . . . . . . 13 |- ( w = ( x i^i ( A X. A ) ) -> ( w o. w ) = ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) )
167	166	sseq1d 3491	. . . . . . . . . . . 12 |- ( 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 ) ) ) )
168	167	rspcev 3182	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
169	147, 164, 168	syl2anc 665	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) )
170		ustexhalf 21211	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> E. x e. U ( x o. x ) C_ u )
171	170	adantlr 719	. . . . . . . . . 10 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) -> E. x e. U ( x o. x ) C_ u )
172	169, 171	r19.29a 2970	. . . . . . . . 9 |- ( ( ( 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 ) ) )
173	94, 98, 95, 172	syl21anc 1263	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
174	123	sseq2d 3492	. . . . . . . . 9 |- ( ( ( ( ( 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 ) ) ) )
175	174	rexbidv 2939	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) ) )
176	173, 175	mpbird 235	. . . . . . 7 |- ( ( ( ( ( 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 )
177	176, 61	r19.29a 2970	. . . . . 6 |- ( ( ( 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 )
178	125, 142, 177	3jca 1185	. . . . 5 |- ( ( ( 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 ) )
179	65, 93, 178	3jca 1185	. . . 4 |- ( ( ( 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 ) ) )
180	179	ralrimiva 2839	. . 3 |- ( ( 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 ) ) )
181	2, 20, 180	3jca 1185	. 2 |- ( ( 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 ) ) ) )
182		isust 21204	. . 3 |- ( 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 ) ) ) ) )
183	13, 182	syl 17	. 2 |- ( ( 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 ) ) ) ) )
184	181, 183	mpbird 235	1 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1868   A.wral 2775   E.wrex 2776   _Vcvv 3081   u. cun 3434   i^i cin 3435   C_ wss 3436   ~Pcpw 3979   class class class wbr 4420   _I cid 4759   X. cxp 4847   `'ccnv 4848   dom cdm 4849   |` cres 4851   o. ccom 4853   ` cfv 5597  (class class class)co 6301   ↾_t crest 15306  UnifOncust 21200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-1st 6803  df-2nd 6804  df-rest 15308  df-ust 21201

This theorem is referenced by:  restutop  21238  restutopopn  21239  ressust  21265  ressusp  21266  trcfilu  21295  cfiluweak  21296