Theorem trust 19779

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 14362	. . . 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 3550	. . . . . . . 8 |- ( A C_ X <-> ( X i^i A ) = A )
5	4	biimpi 194	. . . . . . 7 |- ( A C_ X -> ( X i^i A ) = A )
6	5, 5	xpeq12d 4860	. . . . . 6 |- ( A C_ X -> ( ( X i^i A ) X. ( X i^i A ) ) = ( A X. A ) )
7	3, 6	syl5eq 2482	. . . . 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 5712	. . . . . . . 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 4434	. . . . . 6 |- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> A e. _V )
14		xpexg 6502	. . . . . 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 19756	. . . . . 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 14359	. . . . 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 1218	. . . 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 2513	. . 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 754	. . . . . . . . . . 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 766	. . . . . . . . . . . . . 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 3865	. . . . . . . . . . . . 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 4940	. . . . . . . . . . . . . 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 3361	. . . . . . . . . . . 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 19754	. . . . . . . . . . . . 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 3527	. . . . . . . . . . 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 3515	. . . . . . . . . . . 12 |- u C_ ( w u. u )
34		ustssel 19755	. . . . . . . . . . . 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 1218	. . . . . . . . . 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 3337	. . . . . . . . . . . . . 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 3504	. . . . . . . . . . . 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 758	. . . . . . . . . . . . . 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 3386	. . . . . . . . . . . . 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 3524	. . . . . . . . . . . . 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 2471	. . . . . . . . . . 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 3593	. . . . . . . . . . 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 2488	. . . . . . . . . 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 3540	. . . . . . . . . . . 12 |- ( x = ( w u. u ) -> ( x i^i ( A X. A ) ) = ( ( w u. u ) i^i ( A X. A ) ) )
49	48	eqeq2d 2449	. . . . . . . . . . 11 |- ( x = ( w u. u ) -> ( w = ( x i^i ( A X. A ) ) <-> w = ( ( w u. u ) i^i ( A X. A ) ) ) )
50	49	rspcev 3068	. . . . . . . . . 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 14358	. . . . . . . . . 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 1217	. . . . . . . 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 988	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> U e. (UnifOn ` X ) )
56	15	3adant3 1008	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> ( A X. A ) e. _V )
57		simp3 990	. . . . . . . . . . 11 |- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ v e. ( U ↾t ( A X. A ) ) ) -> v e. ( U ↾t ( A X. A ) ) )
58		elrest 14358	. . . . . . . . . . . 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 1217	. . . . . . . . . 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 1187	. . . . . . . . 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 2857	. . . . . . 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 2794	. . . . 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 758	. . . . . . . . . 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 754	. . . . . . . . . 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 19757	. . . . . . . . . 10 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ x e. U ) -> ( u i^i x ) e. U )
71	66, 68, 69, 70	syl3anc 1218	. . . . . . . . 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 755	. . . . . . . . . . 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 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 ) ) ) ) -> w = ( x i^i ( A X. A ) ) )
74	72, 73	ineq12d 3548	. . . . . . . . . 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 3563	. . . . . . . . . 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 2488	. . . . . . . . 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 3540	. . . . . . . . . . 11 |- ( y = ( u i^i x ) -> ( y i^i ( A X. A ) ) = ( ( u i^i x ) i^i ( A X. A ) ) )
78	77	eqeq2d 2449	. . . . . . . . . 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 3068	. . . . . . . . 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 14358	. . . . . . . . 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 1217	. . . . . . 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 1217	. . . . . . . 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 2883	. . . . . . . 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 2859	. . . . . 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 2794	. . . . 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 765	. . . . . . . . . 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 754	. . . . . . . . . 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 19758	. . . . . . . . . 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 766	. . . . . . . . 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 3565	. . . . . . . . . . . . . 14 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ ( _I |` X )
100		resss 5129	. . . . . . . . . . . . . 14 |- ( _I |` X ) C_ _I
101	99, 100	sstri 3360	. . . . . . . . . . . . 13 |- ( ( _I |` X ) i^i ( A X. A ) ) C_ _I
102		iss 5149	. . . . . . . . . . . . 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 3346	. . . . . . . . . . . . . . . . 17 |- ( ( A C_ X /\ u e. A ) -> u e. X )
106		equid 1729	. . . . . . . . . . . . . . . . . 18 |- u = u
107		resieq 5116	. . . . . . . . . . . . . . . . . 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 4291	. . . . . . . . . . . . . . . . 17 |- ( v = u -> ( u ( _I |` X ) v <-> u ( _I |` X ) u ) )
111	110	rspcev 3068	. . . . . . . . . . . . . . . 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 2794	. . . . . . . . . . . . . 14 |- ( A C_ X -> A. u e. A E. v e. A u ( _I |` X ) v )
114		dminxp 5273	. . . . . . . . . . . . . 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 5105	. . . . . . . . . . . 12 |- ( A C_ X -> ( _I |` dom ( ( _I |` X ) i^i ( A X. A ) ) ) = ( _I |` A ) )
117	103, 116	syl5req 2483	. . . . . . . . . . 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 3570	. . . . . . . . . . 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 3385	. . . . . . . . 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 3388	. . . . . . 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 2857	. . . . . 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 19759	. . . . . . . . . 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 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 5239	. . . . . . . . . . 11 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i `' ( A X. A ) )
131		cnvxp 5250	. . . . . . . . . . . 12 |- `' ( A X. A ) = ( A X. A )
132	131	ineq2i 3544	. . . . . . . . . . 11 |- ( `' u i^i `' ( A X. A ) ) = ( `' u i^i ( A X. A ) )
133	130, 132	eqtri 2458	. . . . . . . . . 10 |- `' ( u i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) )
134	129, 133	syl6eq 2486	. . . . . . . . 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 3540	. . . . . . . . . . 11 |- ( x = `' u -> ( x i^i ( A X. A ) ) = ( `' u i^i ( A X. A ) ) )
136	135	eqeq2d 2449	. . . . . . . . . 10 |- ( x = `' u -> ( `' v = ( x i^i ( A X. A ) ) <-> `' v = ( `' u i^i ( A X. A ) ) ) )
137	136	rspcev 3068	. . . . . . . . 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 14358	. . . . . . . . 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 1217	. . . . . . 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 2857	. . . . . 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 765	. . . . . . . . . . . 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 754	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ A C_ X ) /\ u e. U ) /\ x e. U ) /\ ( x o. x ) C_ u ) -> x e. U )
146		elrestr 14359	. . . . . . . . . . . 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 1218	. . . . . . . . . . 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 3565	. . . . . . . . . . . . . . 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 3361	. . . . . . . . . . . . . . 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 3359	. . . . . . . . . . . . . 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 3566	. . . . . . . . . . . . . . 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 3361	. . . . . . . . . . . . . . 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 5215	. . . . . . . . . . . . . 14 |- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
162	160, 161	sstri 3360	. . . . . . . . . . . . 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 3569	. . . . . . . . . . 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 3378	. . . . . . . . . . . 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 3068	. . . . . . . . . . 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 19760	. . . . . . . . . . 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 2857	. . . . . . . . 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 1217	. . . . . . . 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 3379	. . . . . . . . 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 2731	. . . . . . . 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 2857	. . . . . 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 1168	. . . . 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 1168	. . . 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 2794	. . 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 1168	. 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 19753	. . 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 965   = wceq 1369   e. wcel 1756   A.wral 2710   E.wrex 2711   _Vcvv 2967   u. cun 3321   i^i cin 3322   C_ wss 3323   ~Pcpw 3855   class class class wbr 4287   _I cid 4626   X. cxp 4833   `'ccnv 4834   dom cdm 4835   |` cres 4837   o. ccom 4839   ` cfv 5413  (class class class)co 6086   ↾_t crest 14351  UnifOncust 19749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-1st 6572  df-2nd 6573  df-rest 14353  df-ust 19750

This theorem is referenced by:  restutop  19787  restutopopn  19788  ressust  19814  ressusp  19815  trcfilu  19844  cfiluweak  19845