Theorem trust 20858

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 14849	. . . 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 5145	. . . . . 6 |- ( ( X X. X ) i^i ( A X. A ) ) = ( ( X i^i A ) X. ( X i^i A ) )
4		dfss1 3699	. . . . . . . 8 |- ( A C_ X <-> ( X i^i A ) = A )
5	4	biimpi 194	. . . . . . 7 |- ( A C_ X -> ( X i^i A ) = A )
6	5	sqxpeqd 5034	. . . . . 6 |- ( A C_ X -> ( ( X i^i A ) X. ( X i^i A ) ) = ( A X. A ) )
7	3, 6	syl5eq 2510	. . . . 5 |- ( A C_ X -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
8	7	adantl 466	. . . 4 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
9		simpl 457	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> U e. (UnifOn ` X ) )
10		elfvex 5899	. . . . . . . 8 |- ( U e. (UnifOn ` X ) -> X e. _V )
11	10	adantr 465	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> X e. _V )
12		simpr 461	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A C_ X )
13	11, 12	ssexd 4603	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
14		xpexg 6601	. . . . . 6 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
15	13, 13, 14	syl2anc 661	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
16		ustbasel 20835	. . . . . 6 |- ( U e. (UnifOn ` X ) -> ( X X. X ) e. U )
17	16	adantr 465	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( X X. X ) e. U )
18		elrestr 14846	. . . . 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 1228	. . . 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 2546	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. ( U ↾t ( A X. A ) ) )
21	9	ad5antr 733	. . . . . . . . 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 733	. . . . . . . . 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 755	. . . . . . . . . . 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 768	. . . . . . . . . . . . . 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 4025	. . . . . . . . . . . . 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 733	. . . . . . . . . . . . . 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 5117	. . . . . . . . . . . . . 14 |- ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
28	26, 26, 27	syl2anc 661	. . . . . . . . . . . . 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 3509	. . . . . . . . . . . 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 20833	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> u C_ ( X X. X ) )
31	21, 23, 30	syl2anc 661	. . . . . . . . . . . 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 3676	. . . . . . . . . . 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 3664	. . . . . . . . . . . 12 |- u C_ ( w u. u )
34		ustssel 20834	. . . . . . . . . . . 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 1228	. . . . . . . . . 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 3485	. . . . . . . . . . . . . 14 |- ( w C_ ( A X. A ) <-> ( w i^i ( A X. A ) ) = w )
38	25, 37	sylib 196	. . . . . . . . . . . . 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 3653	. . . . . . . . . . . 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 461	. . . . . . . . . . . . . 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 760	. . . . . . . . . . . . . 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 3534	. . . . . . . . . . . . 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 3673	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) C_ w <-> ( w u. ( u i^i ( A X. A ) ) ) = w )
44	42, 43	sylib 196	. . . . . . . . . . . 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 2499	. . . . . . . . . . 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 3753	. . . . . . . . . . 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 2516	. . . . . . . . . 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 3689	. . . . . . . . . . . 12 |- ( x = ( w u. u ) -> ( x i^i ( A X. A ) ) = ( ( w u. u ) i^i ( A X. A ) ) )
49	48	eqeq2d 2471	. . . . . . . . . . 11 |- ( x = ( w u. u ) -> ( w = ( x i^i ( A X. A ) ) <-> w = ( ( w u. u ) i^i ( A X. A ) ) ) )
50	49	rspcev 3210	. . . . . . . . . 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 661	. . . . . . . . 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 14845	. . . . . . . . . 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 485	. . . . . . . . 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 1227	. . . . . . . 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 996	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> U e. (UnifOn ` X ) )
56	15	3adant3 1016	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> ( A X. A ) e. _V )
57		simp3 998	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> v e. ( U ↾t ( A X. A ) ) )
58		elrest 14845	. . . . . . . . . . . 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 484	. . . . . . . . . . 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 1227	. . . . . . . . . 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 1196	. . . . . . . . 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 725	. . . . . . . 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 2999	. . . . . . 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 434	. . . . . 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 2871	. . . . 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 733	. . . . . . . 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 733	. . . . . . . 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 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 ) ) ) ) -> u e. U )
69		simplr 755	. . . . . . . . . 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 20836	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ x e. U ) -> ( u i^i x ) e. U )
71	66, 68, 69, 70	syl3anc 1228	. . . . . . . . 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 756	. . . . . . . . . . 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 757	. . . . . . . . . . 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 3697	. . . . . . . . . 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 3712	. . . . . . . . . 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 2516	. . . . . . . . 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 3689	. . . . . . . . . . 11 |- ( y = ( u i^i x ) -> ( y i^i ( A X. A ) ) = ( ( u i^i x ) i^i ( A X. A ) ) )
78	77	eqeq2d 2471	. . . . . . . . . 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 3210	. . . . . . . . 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 661	. . . . . . . 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 14845	. . . . . . . . 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 485	. . . . . . . 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 1227	. . . . . . 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 465	. . . . . . . 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 725	. . . . . . . . 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 725	. . . . . . . . 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 461	. . . . . . . . 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 484	. . . . . . . . 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 1227	. . . . . . . 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 3025	. . . . . . . 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 664	. . . . . . 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 3001	. . . . . 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 2871	. . . . 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 767	. . . . . . . . . 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 755	. . . . . . . . . 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 20837	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> ( _I |` X ) C_ u )
97	94, 95, 96	syl2anc 661	. . . . . . . . 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 768	. . . . . . . . 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 3714	. . . . . . . . . . . . . 14 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ ( _I |` X )
100		resss 5307	. . . . . . . . . . . . . 14 |- ( _I |` X ) C_ _I
101	99, 100	sstri 3508	. . . . . . . . . . . . 13 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ _I
102		iss 5331	. . . . . . . . . . . . 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 208	. . . . . . . . . . . 12 |- ( ( _I |` X ) i^i ( A X. A ) ) = ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) )
104		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u e. A )
105		ssel2 3494	. . . . . . . . . . . . . . . . 17 |- ( ( A C_ X /\ u e. A ) -> u e. X )
106		equid 1792	. . . . . . . . . . . . . . . . . 18 |- u = u
107		resieq 5294	. . . . . . . . . . . . . . . . . 18 |- ( ( u e. X /\ u e. X ) -> ( u ( _I |` X ) u <-> u = u ) )
108	106, 107	mpbiri 233	. . . . . . . . . . . . . . . . 17 |- ( ( u e. X /\ u e. X ) -> u ( _I |` X ) u )
109	105, 105, 108	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u ( _I |` X ) u )
110		breq2 4460	. . . . . . . . . . . . . . . . 17 |- ( v = u -> ( u ( _I |` X ) v <-> u ( _I |` X ) u ) )
111	110	rspcev 3210	. . . . . . . . . . . . . . . 16 |- ( ( u e. A /\ u ( _I |` X ) u ) -> E. v e. A u ( _I |` X ) v )
112	104, 109, 111	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( A C_ X /\ u e. A ) -> E. v e. A u ( _I |` X ) v )
113	112	ralrimiva 2871	. . . . . . . . . . . . . 14 |- ( A C_ X -> A. u e. A E. v e. A u ( _I |` X ) v )
114		dminxp 5454	. . . . . . . . . . . . . 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 212	. . . . . . . . . . . . 13 |- ( A C_ X -> dom ( ( _I |` X ) i^i ( A X. A ) ) = A )
116	115	reseq2d 5283	. . . . . . . . . . . 12 |- ( A C_ X -> ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) ) = ( _I |` A ) )
117	103, 116	syl5req 2511	. . . . . . . . . . 11 |- ( A C_ X -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
118	117	adantl 466	. . . . . . . . . 10 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
119		ssrin 3719	. . . . . . . . . . 11 |- ( ( _I |` X ) C_ u -> ( ( _I |` X ) i^i ( A X. A ) ) C_ ( u i^i ( A X. A ) ) )
120	119	adantr 465	. . . . . . . . . 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 3533	. . . . . . . . 9 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) C_ ( u i^i ( A X. A ) ) )
122	97, 98, 121	syl2anc 661	. . . . . . . 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 461	. . . . . . . 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 3536	. . . . . . 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 2999	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ v e. ( U ↾t ( A X. A ) ) ) -> ( _I |` A ) C_ v )
126	15	ad3antrrr 729	. . . . . . . 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 20838	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> `' u e. U )
128	94, 95, 127	syl2anc 661	. . . . . . . . 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 5188	. . . . . . . . . 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 5420	. . . . . . . . . . 11 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i `' ( A X. A ) )
131		cnvxp 5431	. . . . . . . . . . . 12 |- `' ( A X. A ) = ( A X. A )
132	131	ineq2i 3693	. . . . . . . . . . 11 |- ( `' u i^i `' ( A X. A ) ) = ( `' u i^i ( A X. A ) )
133	130, 132	eqtri 2486	. . . . . . . . . 10 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) )
134	129, 133	syl6eq 2514	. . . . . . . . 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 3689	. . . . . . . . . . 11 |- ( x = `' u -> ( x i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) ) )
136	135	eqeq2d 2471	. . . . . . . . . 10 |- ( x = `' u -> ( `' v = ( x i^i ( A X. A ) ) <-> `' v = ( `' u i^i ( A X. A ) ) ) )
137	136	rspcev 3210	. . . . . . . . 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 661	. . . . . . . 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 14845	. . . . . . . . 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 485	. . . . . . . 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 1227	. . . . . . 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 2999	. . . . . 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 767	. . . . . . . . . . . 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 729	. . . . . . . . . . . 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 755	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> x e. U )
146		elrestr 14846	. . . . . . . . . . . 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 1228	. . . . . . . . . . 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 3714	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ x
149		coss1 5168	. . . . . . . . . . . . . . . 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 5169	. . . . . . . . . . . . . . . 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 3509	. . . . . . . . . . . . . . 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 3507	. . . . . . . . . . . . . 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 670	. . . . . . . . . . . . 13 |- ( ( x o. x ) C_ u -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ u )
155	154	adantl 466	. . . . . . . . . . . 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 3715	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ ( A X. A )
157		coss1 5168	. . . . . . . . . . . . . . . 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 5169	. . . . . . . . . . . . . . . 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 3509	. . . . . . . . . . . . . . 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 5399	. . . . . . . . . . . . . 14 |- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
162	160, 161	sstri 3508	. . . . . . . . . . . . 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 3718	. . . . . . . . . . 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 22	. . . . . . . . . . . . . 14 |- ( w = ( x i^i ( A X. A ) ) -> w = ( x i^i ( A X. A ) ) )
166	165, 165	coeq12d 5177	. . . . . . . . . . . . 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 3526	. . . . . . . . . . . 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 3210	. . . . . . . . . . 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 661	. . . . . . . . . 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 20839	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> E. x e. U ( x o. x ) C_ u )
171	170	adantlr 714	. . . . . . . . . 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 2999	. . . . . . . . 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 1227	. . . . . . . 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 3527	. . . . . . . . 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 2968	. . . . . . . 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 232	. . . . . . 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 2999	. . . . . 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 1176	. . . . 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 1176	. . . 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 2871	. . 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 1176	. 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 20832	. . 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 232	1 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1395   e. wcel 1819   A.wral 2807   E.wrex 2808   _Vcvv 3109   u. cun 3469   i^i cin 3470   C_ wss 3471   ~Pcpw 4015   class class class wbr 4456   _I cid 4799   X. cxp 5006   `'ccnv 5007   dom cdm 5008   |` cres 5010   o. ccom 5012   ` cfv 5594  (class class class)co 6296   ↾_t crest 14838  UnifOncust 20828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6799  df-2nd 6800  df-rest 14840  df-ust 20829

This theorem is referenced by:  restutop  20866  restutopopn  20867  ressust  20893  ressusp  20894  trcfilu  20923  cfiluweak  20924