Theorem trust 22837

Description: The trace of a uniform structure 𝑈 on a subset 𝐴 is a uniform structure on 𝐴. Definition 3 of [BourbakiTop1] p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017.)

Assertion

Ref	Expression
trust	⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))

Proof of Theorem trust

Dummy variables 𝑣 𝑢 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		restsspw 16704	. . . 4 ⊢ (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴)
2	1	a1i 11	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴))
3		inxp 5702	. . . . . 6 ⊢ ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴))
4		sseqin2 4191	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
5	4	biimpi 218	. . . . . . 7 ⊢ (𝐴 ⊆ 𝑋 → (𝑋 ∩ 𝐴) = 𝐴)
6	5	sqxpeqd 5586	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴)) = (𝐴 × 𝐴))
7	3, 6	syl5eq 2868	. . . . 5 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
8	7	adantl 484	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
9		simpl 485	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
10		elfvex 6702	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
11	10	adantr 483	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
12		simpr 487	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
13	11, 12	ssexd 5227	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	13, 13	xpexd 7473	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ V)
15		ustbasel 22814	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
16	15	adantr 483	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
17		elrestr 16701	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ (𝑋 × 𝑋) ∈ 𝑈) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
18	9, 14, 16, 17	syl3anc 1367	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
19	8, 18	eqeltrrd 2914	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
20	9	ad5antr 732	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
21	14	ad5antr 732	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
22		simplr 767	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
23		simp-4r 782	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ 𝒫 (𝐴 × 𝐴))
24	23	elpwid 4549	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝐴 × 𝐴))
25	12	ad5antr 732	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
26		xpss12 5569	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
27	25, 25, 26	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
28	24, 27	sstrd 3976	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝑋 × 𝑋))
29		ustssxp 22812	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → 𝑢 ⊆ (𝑋 × 𝑋))
30	20, 22, 29	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ⊆ (𝑋 × 𝑋))
31	28, 30	unssd 4161	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋))
32		ssun2 4148	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑤 ∪ 𝑢)
33		ustssel 22813	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑢 ⊆ (𝑤 ∪ 𝑢) → (𝑤 ∪ 𝑢) ∈ 𝑈))
34	32, 33	mpi 20	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑤 ∪ 𝑢) ∈ 𝑈)
35	20, 22, 31, 34	syl3anc 1367	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ∈ 𝑈)
36		df-ss 3951	. . . . . . . . . . . . . 14 ⊢ (𝑤 ⊆ (𝐴 × 𝐴) ↔ (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
37	24, 36	sylib 220	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
38	37	uneq1d 4137	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))) = (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))))
39		simpr 487	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
40		simpllr 774	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 ⊆ 𝑤)
41	39, 40	eqsstrrd 4005	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤)
42		ssequn2 4158	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤 ↔ (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
43	41, 42	sylib 220	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
44	38, 43	eqtr2d 2857	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))))
45		indir 4251	. . . . . . . . . . 11 ⊢ ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)) = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴)))
46	44, 45	syl6eqr 2874	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
47		ineq1 4180	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑤 ∪ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
48	47	rspceeqv 3637	. . . . . . . . . 10 ⊢ (((𝑤 ∪ 𝑢) ∈ 𝑈 ∧ 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
49	35, 46, 48	syl2anc 586	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
50		elrest 16700	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
51	50	biimpar 480	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
52	20, 21, 49, 51	syl21anc 835	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
53		elrest 16700	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))))
54	53	biimpa 479	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
55	14, 54	syldanl 603	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
56	55	ad2antrr 724	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
57	52, 56	r19.29a 3289	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
58	57	ex 415	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) → (𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
59	58	ralrimiva 3182	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
60	9	ad5antr 732	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑈 ∈ (UnifOn‘𝑋))
61	14	ad5antr 732	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝐴 × 𝐴) ∈ V)
62		simpllr 774	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑢 ∈ 𝑈)
63		simplr 767	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑥 ∈ 𝑈)
64		ustincl 22815	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) → (𝑢 ∩ 𝑥) ∈ 𝑈)
65	60, 62, 63, 64	syl3anc 1367	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑢 ∩ 𝑥) ∈ 𝑈)
66		simprl 769	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
67		simprr 771	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
68	66, 67	ineq12d 4189	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴))))
69		inindir 4203	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴)))
70	68, 69	syl6eqr 2874	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
71		ineq1 4180	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑥) → (𝑦 ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
72	71	rspceeqv 3637	. . . . . . . . 9 ⊢ (((𝑢 ∩ 𝑥) ∈ 𝑈 ∧ (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
73	65, 70, 72	syl2anc 586	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
74		elrest 16700	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → ((𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))))
75	74	biimpar 480	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
76	60, 61, 73, 75	syl21anc 835	. . . . . . 7 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
77	55	adantr 483	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
78	9	ad2antrr 724	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
79	14	ad2antrr 724	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
80		simpr 487	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
81	50	biimpa 479	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
82	78, 79, 80, 81	syl21anc 835	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
83		reeanv 3367	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) ↔ (∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
84	77, 82, 83	sylanbrc 585	. . . . . . 7 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
85	76, 84	r19.29vva 3336	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
86	85	ralrimiva 3182	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
87		simp-4l 781	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
88		simplr 767	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
89		ustdiag 22816	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑢)
90	87, 88, 89	syl2anc 586	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝑋) ⊆ 𝑢)
91		simp-4r 782	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
92		inss1 4204	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ ( I ↾ 𝑋)
93		resss 5877	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝑋) ⊆ I
94	92, 93	sstri 3975	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I
95		iss 5902	. . . . . . . . . . . . 13 ⊢ ((( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I ↔ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))))
96	94, 95	mpbi 232	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
97		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
98		ssel2 3961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝑋)
99		equid 2015	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑢 = 𝑢
100		resieq 5863	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑢( I ↾ 𝑋)𝑢 ↔ 𝑢 = 𝑢))
101	99, 100	mpbiri 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → 𝑢( I ↾ 𝑋)𝑢)
102	98, 98, 101	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢( I ↾ 𝑋)𝑢)
103		breq2 5069	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑢 → (𝑢( I ↾ 𝑋)𝑣 ↔ 𝑢( I ↾ 𝑋)𝑢))
104	103	rspcev 3622	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑢( I ↾ 𝑋)𝑢) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
105	97, 102, 104	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
106	105	ralrimiva 3182	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝑋 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
107		dminxp 6036	. . . . . . . . . . . . . 14 ⊢ (dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
108	106, 107	sylibr 236	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑋 → dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴)
109	108	reseq2d 5852	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))) = ( I ↾ 𝐴))
110	96, 109	syl5req 2869	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
111	110	adantl 484	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
112		ssrin 4209	. . . . . . . . . . 11 ⊢ (( I ↾ 𝑋) ⊆ 𝑢 → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
113	112	adantr 483	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
114	111, 113	eqsstrd 4004	. . . . . . . . 9 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
115	90, 91, 114	syl2anc 586	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
116		simpr 487	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
117	115, 116	sseqtrrd 4007	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
118	117, 55	r19.29a 3289	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
119	14	ad3antrrr 728	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
120		ustinvel 22817	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ◡𝑢 ∈ 𝑈)
121	87, 88, 120	syl2anc 586	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑢 ∈ 𝑈)
122	116	cnveqd 5745	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = ◡(𝑢 ∩ (𝐴 × 𝐴)))
123		cnvin 6002	. . . . . . . . . . 11 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ ◡(𝐴 × 𝐴))
124		cnvxp 6013	. . . . . . . . . . . 12 ⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴)
125	124	ineq2i 4185	. . . . . . . . . . 11 ⊢ (◡𝑢 ∩ ◡(𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
126	123, 125	eqtri 2844	. . . . . . . . . 10 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
127	122, 126	syl6eq 2872	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴)))
128		ineq1 4180	. . . . . . . . . 10 ⊢ (𝑥 = ◡𝑢 → (𝑥 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴)))
129	128	rspceeqv 3637	. . . . . . . . 9 ⊢ ((◡𝑢 ∈ 𝑈 ∧ ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
130	121, 127, 129	syl2anc 586	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
131		elrest 16700	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))))
132	131	biimpar 480	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
133	87, 119, 130, 132	syl21anc 835	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
134	133, 55	r19.29a 3289	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
135		simp-4l 781	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑈 ∈ (UnifOn‘𝑋))
136	14	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝐴 × 𝐴) ∈ V)
137		simplr 767	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑥 ∈ 𝑈)
138		elrestr 16701	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑥 ∈ 𝑈) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
139	135, 136, 137, 138	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
140		inss1 4204	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥
141		coss1 5725	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))))
142		coss2 5726	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
143	141, 142	sstrd 3976	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
144	140, 143	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥)
145		sstr 3974	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
146	144, 145	mpan 688	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘ 𝑥) ⊆ 𝑢 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
147	146	adantl 484	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
148		inss2 4205	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
149		coss1 5725	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
150		coss2 5726	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
151	149, 150	sstrd 3976	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
152	148, 151	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))
153		xpidtr 5981	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
154	152, 153	sstri 3975	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)
155	154	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))
156	147, 155	ssind 4208	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
157		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
158	157, 157	coeq12d 5734	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → (𝑤 ∘ 𝑤) = ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
159	158	sseq1d 3997	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → ((𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)) ↔ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
160	159	rspcev 3622	. . . . . . . . . . 11 ⊢ (((𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
161	139, 156, 160	syl2anc 586	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
162		ustexhalf 22818	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
163	162	adantlr 713	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
164	161, 163	r19.29a 3289	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
165	164	ad4ant13 749	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
166	116	sseq2d 3998	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ (𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
167	166	rexbidv 3297	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
168	165, 167	mpbird 259	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
169	168, 55	r19.29a 3289	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
170	118, 134, 169	3jca 1124	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))
171	59, 86, 170	3jca 1124	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
172	171	ralrimiva 3182	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
173	2, 19, 172	3jca 1124	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))))
174		isust 22811	. . 3 ⊢ (𝐴 ∈ V → ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) ↔ ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))))
175	13, 174	syl 17	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) ↔ ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))))
176	173, 175	mpbird 259	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139  Vcvv 3494   ∪ cun 3933   ∩ cin 3934   ⊆ wss 3935  𝒫 cpw 4538   class class class wbr 5065   I cid 5458   × cxp 5552  ^◡ccnv 5553  dom cdm 5554   ↾ cres 5556   ∘ ccom 5558  ‘cfv 6354  (class class class)co 7155   ↾_t crest 16693  UnifOncust 22807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-ov 7158  df-oprab 7159  df-mpo 7160  df-1st 7688  df-2nd 7689  df-rest 16695  df-ust 22808

This theorem is referenced by:  restutop  22845  restutopopn  22846  ressust  22872  ressusp  22873  trcfilu  22902  cfiluweak  22903