Theorem trust 21244

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 15330	. . . 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 4967	. . . . . 6 |- ( ( X X. X ) i^i ( A X. A ) ) = ( ( X i^i A ) X. ( X i^i A ) )
4		dfss1 3637	. . . . . . . 8 |- ( A C_ X <-> ( X i^i A ) = A )
5	4	biimpi 198	. . . . . . 7 |- ( A C_ X -> ( X i^i A ) = A )
6	5	sqxpeqd 4860	. . . . . 6 |- ( A C_ X -> ( ( X i^i A ) X. ( X i^i A ) ) = ( A X. A ) )
7	3, 6	syl5eq 2497	. . . . 5 |- ( A C_ X -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
8	7	adantl 468	. . . 4 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( ( X X. X ) i^i ( A X. A ) ) = ( A X. A ) )
9		simpl 459	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> U e. (UnifOn ` X ) )
10		elfvex 5892	. . . . . . . 8 |- ( U e. (UnifOn ` X ) -> X e. _V )
11	10	adantr 467	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> X e. _V )
12		simpr 463	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A C_ X )
13	11, 12	ssexd 4550	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
14		xpexg 6593	. . . . . 6 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
15	13, 13, 14	syl2anc 667	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
16		ustbasel 21221	. . . . . 6 |- ( U e. (UnifOn ` X ) -> ( X X. X ) e. U )
17	16	adantr 467	. . . . 5 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( X X. X ) e. U )
18		elrestr 15327	. . . . 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 1268	. . . 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 2530	. . 3 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( A X. A ) e. ( U ↾t ( A X. A ) ) )
21	9	ad5antr 740	. . . . . . . . 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 740	. . . . . . . . 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 762	. . . . . . . . . . 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 777	. . . . . . . . . . . . . 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 3961	. . . . . . . . . . . . 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 740	. . . . . . . . . . . . . 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 667	. . . . . . . . . . . . 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 3442	. . . . . . . . . . . 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 21219	. . . . . . . . . . . . 13 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> u C_ ( X X. X ) )
31	21, 23, 30	syl2anc 667	. . . . . . . . . . . 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 3610	. . . . . . . . . . 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 3598	. . . . . . . . . . . 12 |- u C_ ( w u. u )
34		ustssel 21220	. . . . . . . . . . . 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 20	. . . . . . . . . . 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 1268	. . . . . . . . . 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 3418	. . . . . . . . . . . . . 14 |- ( w C_ ( A X. A ) <-> ( w i^i ( A X. A ) ) = w )
38	25, 37	sylib 200	. . . . . . . . . . . . 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 3587	. . . . . . . . . . . 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 463	. . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . 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 3467	. . . . . . . . . . . . 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 3607	. . . . . . . . . . . . 13 |- ( ( u i^i ( A X. A ) ) C_ w <-> ( w u. ( u i^i ( A X. A ) ) ) = w )
44	42, 43	sylib 200	. . . . . . . . . . . 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 2486	. . . . . . . . . . 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 3691	. . . . . . . . . . 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 2503	. . . . . . . . . 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 3627	. . . . . . . . . . . 12 |- ( x = ( w u. u ) -> ( x i^i ( A X. A ) ) = ( ( w u. u ) i^i ( A X. A ) ) )
49	48	eqeq2d 2461	. . . . . . . . . . 11 |- ( x = ( w u. u ) -> ( w = ( x i^i ( A X. A ) ) <-> w = ( ( w u. u ) i^i ( A X. A ) ) ) )
50	49	rspcev 3150	. . . . . . . . . 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 667	. . . . . . . . 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 15326	. . . . . . . . . 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 488	. . . . . . . . 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 1267	. . . . . . . 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 1008	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> U e. (UnifOn ` X ) )
56	15	3adant3 1028	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> ( A X. A ) e. _V )
57		simp3 1010	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> v e. ( U ↾t ( A X. A ) ) )
58		elrest 15326	. . . . . . . . . . . 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 487	. . . . . . . . . . 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 1267	. . . . . . . . . 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 1208	. . . . . . . . 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 732	. . . . . . . 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 2932	. . . . . . 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 436	. . . . . 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 2802	. . . . 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 740	. . . . . . . 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 740	. . . . . . . 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 769	. . . . . . . . . 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 762	. . . . . . . . . 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 21222	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ x e. U ) -> ( u i^i x ) e. U )
71	66, 68, 69, 70	syl3anc 1268	. . . . . . . . 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 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 ) ) ) ) -> v = ( u i^i ( A X. A ) ) )
73		simprr 766	. . . . . . . . . . 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 3635	. . . . . . . . . 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 3650	. . . . . . . . . 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 2503	. . . . . . . . 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 3627	. . . . . . . . . . 11 |- ( y = ( u i^i x ) -> ( y i^i ( A X. A ) ) = ( ( u i^i x ) i^i ( A X. A ) ) )
78	77	eqeq2d 2461	. . . . . . . . . 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 3150	. . . . . . . . 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 667	. . . . . . . 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 15326	. . . . . . . . 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 488	. . . . . . . 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 1267	. . . . . . 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 467	. . . . . . . 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 732	. . . . . . . . 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 732	. . . . . . . . 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 463	. . . . . . . . 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 487	. . . . . . . . 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 1267	. . . . . . . 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 2958	. . . . . . . 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 670	. . . . . . 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 2934	. . . . . 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 2802	. . . . 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 776	. . . . . . . . . 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 762	. . . . . . . . . 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 21223	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> ( _I |` X ) C_ u )
97	94, 95, 96	syl2anc 667	. . . . . . . . 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 777	. . . . . . . . 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 3652	. . . . . . . . . . . . . 14 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ ( _I |` X )
100		resss 5128	. . . . . . . . . . . . . 14 |- ( _I |` X ) C_ _I
101	99, 100	sstri 3441	. . . . . . . . . . . . 13 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ _I
102		iss 5152	. . . . . . . . . . . . 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 212	. . . . . . . . . . . 12 |- ( ( _I |` X ) i^i ( A X. A ) ) = ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) )
104		simpr 463	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u e. A )
105		ssel2 3427	. . . . . . . . . . . . . . . . 17 |- ( ( A C_ X /\ u e. A ) -> u e. X )
106		equid 1855	. . . . . . . . . . . . . . . . . 18 |- u = u
107		resieq 5115	. . . . . . . . . . . . . . . . . 18 |- ( ( u e. X /\ u e. X ) -> ( u ( _I |` X ) u <-> u = u ) )
108	106, 107	mpbiri 237	. . . . . . . . . . . . . . . . 17 |- ( ( u e. X /\ u e. X ) -> u ( _I |` X ) u )
109	105, 105, 108	syl2anc 667	. . . . . . . . . . . . . . . 16 |- ( ( A C_ X /\ u e. A ) -> u ( _I |` X ) u )
110		breq2 4406	. . . . . . . . . . . . . . . . 17 |- ( v = u -> ( u ( _I |` X ) v <-> u ( _I |` X ) u ) )
111	110	rspcev 3150	. . . . . . . . . . . . . . . 16 |- ( ( u e. A /\ u ( _I |` X ) u ) -> E. v e. A u ( _I |` X ) v )
112	104, 109, 111	syl2anc 667	. . . . . . . . . . . . . . 15 |- ( ( A C_ X /\ u e. A ) -> E. v e. A u ( _I |` X ) v )
113	112	ralrimiva 2802	. . . . . . . . . . . . . 14 |- ( A C_ X -> A. u e. A E. v e. A u ( _I |` X ) v )
114		dminxp 5277	. . . . . . . . . . . . . 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 216	. . . . . . . . . . . . 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 2498	. . . . . . . . . . 11 |- ( A C_ X -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
118	117	adantl 468	. . . . . . . . . 10 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) = ( ( _I |` X ) i^i ( A X. A ) ) )
119		ssrin 3657	. . . . . . . . . . 11 |- ( ( _I |` X ) C_ u -> ( ( _I |` X ) i^i ( A X. A ) ) C_ ( u i^i ( A X. A ) ) )
120	119	adantr 467	. . . . . . . . . 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 3466	. . . . . . . . 9 |- ( ( ( _I |` X ) C_ u /\ A C_ X ) -> ( _I |` A ) C_ ( u i^i ( A X. A ) ) )
122	97, 98, 121	syl2anc 667	. . . . . . . 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 463	. . . . . . . 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 3469	. . . . . . 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 2932	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ v e. ( U ↾t ( A X. A ) ) ) -> ( _I |` A ) C_ v )
126	15	ad3antrrr 736	. . . . . . . 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 21224	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> `' u e. U )
128	94, 95, 127	syl2anc 667	. . . . . . . . 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 5010	. . . . . . . . . 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 5243	. . . . . . . . . . 11 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i `' ( A X. A ) )
131		cnvxp 5254	. . . . . . . . . . . 12 |- `' ( A X. A ) = ( A X. A )
132	131	ineq2i 3631	. . . . . . . . . . 11 |- ( `' u i^i `' ( A X. A ) ) = ( `' u i^i ( A X. A ) )
133	130, 132	eqtri 2473	. . . . . . . . . 10 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) )
134	129, 133	syl6eq 2501	. . . . . . . . 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 3627	. . . . . . . . . . 11 |- ( x = `' u -> ( x i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) ) )
136	135	eqeq2d 2461	. . . . . . . . . 10 |- ( x = `' u -> ( `' v = ( x i^i ( A X. A ) ) <-> `' v = ( `' u i^i ( A X. A ) ) ) )
137	136	rspcev 3150	. . . . . . . . 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 667	. . . . . . . 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 15326	. . . . . . . . 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 488	. . . . . . . 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 1267	. . . . . . 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 2932	. . . . . 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 776	. . . . . . . . . . . 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 736	. . . . . . . . . . . 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 762	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> x e. U )
146		elrestr 15327	. . . . . . . . . . . 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 1268	. . . . . . . . . . 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 3652	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ x
149		coss1 4990	. . . . . . . . . . . . . . . 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 4991	. . . . . . . . . . . . . . . 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 3442	. . . . . . . . . . . . . . 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 3440	. . . . . . . . . . . . . 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 676	. . . . . . . . . . . . 13 |- ( ( x o. x ) C_ u -> ( ( x i^i ( A X. A ) ) o. ( x i^i ( A X. A ) ) ) C_ u )
155	154	adantl 468	. . . . . . . . . . . 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 3653	. . . . . . . . . . . . . . 15 |- ( x i^i ( A X. A ) ) C_ ( A X. A )
157		coss1 4990	. . . . . . . . . . . . . . . 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 4991	. . . . . . . . . . . . . . . 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 3442	. . . . . . . . . . . . . . 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 5222	. . . . . . . . . . . . . 14 |- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
162	160, 161	sstri 3441	. . . . . . . . . . . . 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 3656	. . . . . . . . . . 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 4999	. . . . . . . . . . . . 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 3459	. . . . . . . . . . . 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 3150	. . . . . . . . . . 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 667	. . . . . . . . . 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 21225	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> E. x e. U ( x o. x ) C_ u )
171	170	adantlr 721	. . . . . . . . . 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 2932	. . . . . . . . 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 1267	. . . . . . . 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 3460	. . . . . . . . 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 2901	. . . . . . . 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 236	. . . . . . 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 2932	. . . . . 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 1188	. . . . 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 1188	. . . 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 2802	. . 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 1188	. 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 21218	. . 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 236	1 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   A.wral 2737   E.wrex 2738   _Vcvv 3045   u. cun 3402   i^i cin 3403   C_ wss 3404   ~Pcpw 3951   class class class wbr 4402   _I cid 4744   X. cxp 4832   `'ccnv 4833   dom cdm 4834   |` cres 4836   o. ccom 4838   ` cfv 5582  (class class class)co 6290   ↾_t crest 15319  UnifOncust 21214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-rest 15321  df-ust 21215

This theorem is referenced by:  restutop  21252  restutopopn  21253  ressust  21279  ressusp  21280  trcfilu  21309  cfiluweak  21310