Theorem trust 18212

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 13614	. . . 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 4966	. . . . . 6 |- ( ( X X. X ) i^i ( A X. A ) ) = ( ( X i^i A ) X. ( X i^i A ) )
4		dfss1 3505	. . . . . . . 8 |- ( A C_ X <-> ( X i^i A ) = A )
5	4	biimpi 187	. . . . . . 7 |- ( A C_ X -> ( X i^i A ) = A )
6	5, 5	xpeq12d 4862	. . . . . 6 |- ( A C_ X -> ( ( X i^i A ) X. ( X i^i A ) ) = ( A X. A ) )
7	3, 6	syl5eq 2448	. . . . 5 |- ( A C_ X -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
8	7	adantl 453	. . . 4 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
9		simpl 444	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> U e. (UnifOn ` X ) )
10		elfvex 5717	. . . . . . . 8 |- ( U e. (UnifOn ` X ) -> X e. _V )
11	10	adantr 452	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> X e. _V )
12		simpr 448	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A C_ X )
13	11, 12	ssexd 4310	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
14		xpexg 4948	. . . . . 6 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
15	13, 13, 14	syl2anc 643	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
16		ustbasel 18189	. . . . . 6 |- ( U e. (UnifOn ` X ) -> ( X X. X ) e. U )
17	16	adantr 452	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( X X. X ) e. U )
18		elrestr 13611	. . . . 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 1184	. . . 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 2479	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. ( U ↾t ( A X. A ) ) )
21	9	ad5antr 715	. . . . . . . . 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 715	. . . . . . . . 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 732	. . . . . . . . . . 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 744	. . . . . . . . . . . . . 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 3768	. . . . . . . . . . . . 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 715	. . . . . . . . . . . . . 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 4940	. . . . . . . . . . . . . 14 |- ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
28	26, 26, 27	syl2anc 643	. . . . . . . . . . . . 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 3318	. . . . . . . . . . . 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 18187	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> u C_ ( X X. X ) )
31	21, 23, 30	syl2anc 643	. . . . . . . . . . . 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 3483	. . . . . . . . . . 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 3471	. . . . . . . . . . . 12 |- u C_ ( w u. u )
34		ustssel 18188	. . . . . . . . . . . 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 17	. . . . . . . . . . 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 1184	. . . . . . . . . 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 3294	. . . . . . . . . . . . . 14 |- ( w C_ ( A X. A ) <-> ( w i^i ( A X. A ) ) = w )
38	25, 37	sylib 189	. . . . . . . . . . . . 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 3460	. . . . . . . . . . . 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 448	. . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . 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 3343	. . . . . . . . . . . . 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 3480	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) C_ w <-> ( w u. ( u i^i ( A X. A ) ) ) = w )
44	42, 43	sylib 189	. . . . . . . . . . . 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 2437	. . . . . . . . . . 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 3549	. . . . . . . . . . 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 2454	. . . . . . . . . 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 3495	. . . . . . . . . . . 12 |- ( x = ( w u. u ) -> ( x i^i ( A X. A ) ) = ( ( w u. u ) i^i ( A X. A ) ) )
49	48	eqeq2d 2415	. . . . . . . . . . 11 |- ( x = ( w u. u ) -> ( w = ( x i^i ( A X. A ) ) <-> w = ( ( w u. u ) i^i ( A X. A ) ) ) )
50	49	rspcev 3012	. . . . . . . . . 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 643	. . . . . . . . 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 13610	. . . . . . . . . 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 472	. . . . . . . . 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 1183	. . . . . . . 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 957	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> U e. (UnifOn ` X ) )
56	15	3adant3 977	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> ( A X. A ) e. _V )
57		simp3 959	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> v e. ( U ↾t ( A X. A ) ) )
58		elrest 13610	. . . . . . . . . . . 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 471	. . . . . . . . . . 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 1183	. . . . . . . . . 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 1153	. . . . . . . . 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 707	. . . . . . . 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 2810	. . . . . . 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 424	. . . . . 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 2749	. . . . 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 715	. . . . . . . 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 715	. . . . . . . 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 736	. . . . . . . . . 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 732	. . . . . . . . . 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 18190	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ x e. U ) -> ( u i^i x ) e. U )
71	66, 68, 69, 70	syl3anc 1184	. . . . . . . . 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 733	. . . . . . . . . . 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 734	. . . . . . . . . . 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 3503	. . . . . . . . . 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 3519	. . . . . . . . . 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 2454	. . . . . . . . 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 3495	. . . . . . . . . . 11 |- ( y = ( u i^i x ) -> ( y i^i ( A X. A ) ) = ( ( u i^i x ) i^i ( A X. A ) ) )
78	77	eqeq2d 2415	. . . . . . . . . 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 3012	. . . . . . . . 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 643	. . . . . . . 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 13610	. . . . . . . . 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 472	. . . . . . . 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 1183	. . . . . . 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 452	. . . . . . . 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 707	. . . . . . . . 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 707	. . . . . . . . 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 448	. . . . . . . . 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 471	. . . . . . . . 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 1183	. . . . . . . 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 2835	. . . . . . . 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 646	. . . . . . 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.29_2a 2812	. . . . . 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 2749	. . . . 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 743	. . . . . . . . . 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 732	. . . . . . . . . 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 18191	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> ( _I |` X ) C_ u )
97	94, 95, 96	syl2anc 643	. . . . . . . . 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 744	. . . . . . . . 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 3521	. . . . . . . . . . . . . 14 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ ( _I |` X )
100		resss 5129	. . . . . . . . . . . . . 14 |- ( _I |` X ) C_ _I
101	99, 100	sstri 3317	. . . . . . . . . . . . 13 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ _I
102		iss 5148	. . . . . . . . . . . . 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 200	. . . . . . . . . . . 12 |- ( ( _I |` X ) i^i ( A X. A ) ) = ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) )
104		simpr 448	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u e. A )
105		ssel2 3303	. . . . . . . . . . . . . . . . 17 |- ( ( A C_ X /\ u e. A ) -> u e. X )
106		equid 1684	. . . . . . . . . . . . . . . . . 18 |- u = u
107		resieq 5115	. . . . . . . . . . . . . . . . . 18 |- ( ( u e. X /\ u e. X ) -> ( u ( _I |` X ) u <-> u = u ) )
108	106, 107	mpbiri 225	. . . . . . . . . . . . . . . . 17 |- ( ( u e. X /\ u e. X ) -> u ( _I |` X ) u )
109	105, 105, 108	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u ( _I |` X ) u )
110		breq2 4176	. . . . . . . . . . . . . . . . 17 |- ( v = u -> ( u ( _I |` X ) v <-> u ( _I |` X ) u ) )
111	110	rspcev 3012	. . . . . . . . . . . . . . . 16 |- ( ( u e. A /\ u ( _I |` X ) u ) -> E. v e. A u ( _I |` X ) v )
112	104, 109, 111	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ( A C_ X /\ u e. A ) -> E. v e. A u ( _I |` X ) v )
113	112	ralrimiva 2749	. . . . . . . . . . . . . 14 |- ( A C_ X -> A. u e. A E. v e. A u ( _I |` X ) v )
114		dminxp 5270	. . . . . . . . . . . . . 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 204	. . . . . . . . . . . . 13 |- ( A C_ X -> dom ( ( _I |` X ) i^i ( A X. A ) ) = A )
116	115	reseq2d 5105	. . . . . . . . . . . 12 |- ( A C_ X -> ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) ) = ( _I |` A ) )
117	103, 116	syl5req 2449	. . . . . . . . . . 11 |- ( A C_ X -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
118	117	adantl 453	. . . . . . . . . 10 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
119		ssrin 3526	. . . . . . . . . . 11 |- ( ( _I |` X ) C_ u -> ( ( _I |` X ) i^i ( A X. A ) ) C_ ( u i^i ( A X. A ) ) )
120	119	adantr 452	. . . . . . . . . 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 3342	. . . . . . . . 9 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) C_ ( u i^i ( A X. A ) ) )
122	97, 98, 121	syl2anc 643	. . . . . . . 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 448	. . . . . . . 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 3345	. . . . . . 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 2810	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ v e. ( U ↾t ( A X. A ) ) ) -> ( _I |` A ) C_ v )
126	15	ad3antrrr 711	. . . . . . . 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 18192	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> `' u e. U )
128	94, 95, 127	syl2anc 643	. . . . . . . . 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 5007	. . . . . . . . . 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 5238	. . . . . . . . . . 11 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i `' ( A X. A ) )
131		cnvxp 5249	. . . . . . . . . . . 12 |- `' ( A X. A ) = ( A X. A )
132	131	ineq2i 3499	. . . . . . . . . . 11 |- ( `' u i^i `' ( A X. A ) ) = ( `' u i^i ( A X. A ) )
133	130, 132	eqtri 2424	. . . . . . . . . 10 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) )
134	129, 133	syl6eq 2452	. . . . . . . . 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 3495	. . . . . . . . . . 11 |- ( x = `' u -> ( x i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) ) )
136	135	eqeq2d 2415	. . . . . . . . . 10 |- ( x = `' u -> ( `' v = ( x i^i ( A X. A ) ) <-> `' v = ( `' u i^i ( A X. A ) ) ) )
137	136	rspcev 3012	. . . . . . . . 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 643	. . . . . . . 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 13610	. . . . . . . . 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 472	. . . . . . . 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 1183	. . . . . . 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 2810	. . . . . 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 743	. . . . . . . . . . . 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 711	. . . . . . . . . . . 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 732	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> x e. U )
146		elrestr 13611	. . . . . . . . . . . 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 1184	. . . . . . . . . . 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 3521	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ x
149		coss1 4987	. . . . . . . . . . . . . . . 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 4988	. . . . . . . . . . . . . . . 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 3318	. . . . . . . . . . . . . . 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 8	. . . . . . . . . . . . . 14 |- ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( x o. x )
153		sstr 3316	. . . . . . . . . . . . . 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 652	. . . . . . . . . . . . 13 |- ( ( x o. x ) C_ u -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ u )
155	154	adantl 453	. . . . . . . . . . . 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 3522	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ ( A X. A )
157		coss1 4987	. . . . . . . . . . . . . . . 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 4988	. . . . . . . . . . . . . . . 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 3318	. . . . . . . . . . . . . . 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 8	. . . . . . . . . . . . . 14 |- ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ ( ( A X. A ) o. ( A X. A ) )
161		xpidtr 5215	. . . . . . . . . . . . . 14 |- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
162	160, 161	sstri 3317	. . . . . . . . . . . . 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 3525	. . . . . . . . . . 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 20	. . . . . . . . . . . . . 14 |- ( w = ( x i^i ( A X. A ) ) -> w = ( x i^i ( A X. A ) ) )
166	165, 165	coeq12d 4996	. . . . . . . . . . . . 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 3335	. . . . . . . . . . . 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 3012	. . . . . . . . . . 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 643	. . . . . . . . . 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 18193	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> E. x e. U ( x o. x ) C_ u )
171	170	adantlr 696	. . . . . . . . . 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 2810	. . . . . . . . 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 1183	. . . . . . . 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 3336	. . . . . . . . 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 2687	. . . . . . . 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 224	. . . . . . 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 2810	. . . . . 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 1134	. . . . 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 1134	. . . 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 2749	. . 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 1134	. 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 18186	. . 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 16	. 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 224	1 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   _Vcvv 2916   u. cun 3278   i^i cin 3279   C_ wss 3280   ~Pcpw 3759   class class class wbr 4172   _I cid 4453   X. cxp 4835   `'ccnv 4836   dom cdm 4837   |` cres 4839   o. ccom 4841   ` cfv 5413  (class class class)co 6040   ↾_t crest 13603  UnifOncust 18182

This theorem is referenced by:  restutop  18220  restutopopn  18221  ressust  18247  ressusp  18248  trcfilu  18277  cfiluweak  18278

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-rest 13605  df-ust 18183