Theorem trust 23289

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 17059	. . . 4 ⊢ (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴)
2	1	a1i 11	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴))
3		inxp 5730	. . . . . 6 ⊢ ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴))
4		sseqin2 4146	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
5	4	biimpi 215	. . . . . . 7 ⊢ (𝐴 ⊆ 𝑋 → (𝑋 ∩ 𝐴) = 𝐴)
6	5	sqxpeqd 5612	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴)) = (𝐴 × 𝐴))
7	3, 6	eqtrid 2790	. . . . 5 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
8	7	adantl 481	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
9		simpl 482	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
10		elfvex 6789	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
11	10	adantr 480	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
12		simpr 484	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
13	11, 12	ssexd 5243	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	13, 13	xpexd 7579	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ V)
15		ustbasel 23266	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
16	15	adantr 480	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
17		elrestr 17056	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ (𝑋 × 𝑋) ∈ 𝑈) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
18	9, 14, 16, 17	syl3anc 1369	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
19	8, 18	eqeltrrd 2840	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
20	9	ad5antr 730	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
21	14	ad5antr 730	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
22		simplr 765	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
23		simp-4r 780	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ 𝒫 (𝐴 × 𝐴))
24	23	elpwid 4541	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝐴 × 𝐴))
25	12	ad5antr 730	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
26		xpss12 5595	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
27	25, 25, 26	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
28	24, 27	sstrd 3927	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝑋 × 𝑋))
29		ustssxp 23264	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → 𝑢 ⊆ (𝑋 × 𝑋))
30	20, 22, 29	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ⊆ (𝑋 × 𝑋))
31	28, 30	unssd 4116	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋))
32		ssun2 4103	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑤 ∪ 𝑢)
33		ustssel 23265	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑢 ⊆ (𝑤 ∪ 𝑢) → (𝑤 ∪ 𝑢) ∈ 𝑈))
34	32, 33	mpi 20	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑤 ∪ 𝑢) ∈ 𝑈)
35	20, 22, 31, 34	syl3anc 1369	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ∈ 𝑈)
36		df-ss 3900	. . . . . . . . . . . . . 14 ⊢ (𝑤 ⊆ (𝐴 × 𝐴) ↔ (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
37	24, 36	sylib 217	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
38	37	uneq1d 4092	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))) = (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))))
39		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
40		simpllr 772	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 ⊆ 𝑤)
41	39, 40	eqsstrrd 3956	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤)
42		ssequn2 4113	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤 ↔ (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
43	41, 42	sylib 217	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
44	38, 43	eqtr2d 2779	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))))
45		indir 4206	. . . . . . . . . . 11 ⊢ ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)) = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴)))
46	44, 45	eqtr4di 2797	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
47		ineq1 4136	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑤 ∪ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
48	47	rspceeqv 3567	. . . . . . . . . 10 ⊢ (((𝑤 ∪ 𝑢) ∈ 𝑈 ∧ 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
49	35, 46, 48	syl2anc 583	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
50		elrest 17055	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
51	50	biimpar 477	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
52	20, 21, 49, 51	syl21anc 834	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
53		elrest 17055	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))))
54	53	biimpa 476	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
55	14, 54	syldanl 601	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
56	55	ad2antrr 722	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
57	52, 56	r19.29a 3217	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
58	57	ex 412	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) → (𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
59	58	ralrimiva 3107	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
60	9	ad5antr 730	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑈 ∈ (UnifOn‘𝑋))
61	14	ad5antr 730	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝐴 × 𝐴) ∈ V)
62		simpllr 772	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑢 ∈ 𝑈)
63		simplr 765	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑥 ∈ 𝑈)
64		ustincl 23267	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) → (𝑢 ∩ 𝑥) ∈ 𝑈)
65	60, 62, 63, 64	syl3anc 1369	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑢 ∩ 𝑥) ∈ 𝑈)
66		simprl 767	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
67		simprr 769	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
68	66, 67	ineq12d 4144	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴))))
69		inindir 4158	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴)))
70	68, 69	eqtr4di 2797	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
71		ineq1 4136	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑥) → (𝑦 ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
72	71	rspceeqv 3567	. . . . . . . . 9 ⊢ (((𝑢 ∩ 𝑥) ∈ 𝑈 ∧ (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
73	65, 70, 72	syl2anc 583	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
74		elrest 17055	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → ((𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))))
75	74	biimpar 477	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
76	60, 61, 73, 75	syl21anc 834	. . . . . . 7 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
77	55	adantr 480	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
78	9	ad2antrr 722	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
79	14	ad2antrr 722	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
80		simpr 484	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
81	50	biimpa 476	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
82	78, 79, 80, 81	syl21anc 834	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
83		reeanv 3292	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) ↔ (∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
84	77, 82, 83	sylanbrc 582	. . . . . . 7 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
85	76, 84	r19.29vva 3263	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
86	85	ralrimiva 3107	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
87		simp-4l 779	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
88		simplr 765	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
89		ustdiag 23268	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑢)
90	87, 88, 89	syl2anc 583	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝑋) ⊆ 𝑢)
91		simp-4r 780	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
92		inss1 4159	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ ( I ↾ 𝑋)
93		resss 5905	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝑋) ⊆ I
94	92, 93	sstri 3926	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I
95		iss 5932	. . . . . . . . . . . . 13 ⊢ ((( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I ↔ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))))
96	94, 95	mpbi 229	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
97		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
98		ssel2 3912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝑋)
99		equid 2016	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑢 = 𝑢
100		resieq 5891	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑢( I ↾ 𝑋)𝑢 ↔ 𝑢 = 𝑢))
101	99, 100	mpbiri 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → 𝑢( I ↾ 𝑋)𝑢)
102	98, 98, 101	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢( I ↾ 𝑋)𝑢)
103		breq2 5074	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑢 → (𝑢( I ↾ 𝑋)𝑣 ↔ 𝑢( I ↾ 𝑋)𝑢))
104	103	rspcev 3552	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑢( I ↾ 𝑋)𝑢) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
105	97, 102, 104	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
106	105	ralrimiva 3107	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝑋 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
107		dminxp 6072	. . . . . . . . . . . . . 14 ⊢ (dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
108	106, 107	sylibr 233	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑋 → dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴)
109	108	reseq2d 5880	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))) = ( I ↾ 𝐴))
110	96, 109	eqtr2id 2792	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
111	110	adantl 481	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
112		ssrin 4164	. . . . . . . . . . 11 ⊢ (( I ↾ 𝑋) ⊆ 𝑢 → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
113	112	adantr 480	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
114	111, 113	eqsstrd 3955	. . . . . . . . 9 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
115	90, 91, 114	syl2anc 583	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
116		simpr 484	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
117	115, 116	sseqtrrd 3958	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
118	117, 55	r19.29a 3217	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
119	14	ad3antrrr 726	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
120		ustinvel 23269	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ◡𝑢 ∈ 𝑈)
121	87, 88, 120	syl2anc 583	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑢 ∈ 𝑈)
122	116	cnveqd 5773	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = ◡(𝑢 ∩ (𝐴 × 𝐴)))
123		cnvin 6037	. . . . . . . . . . 11 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ ◡(𝐴 × 𝐴))
124		cnvxp 6049	. . . . . . . . . . . 12 ⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴)
125	124	ineq2i 4140	. . . . . . . . . . 11 ⊢ (◡𝑢 ∩ ◡(𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
126	123, 125	eqtri 2766	. . . . . . . . . 10 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
127	122, 126	eqtrdi 2795	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴)))
128		ineq1 4136	. . . . . . . . . 10 ⊢ (𝑥 = ◡𝑢 → (𝑥 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴)))
129	128	rspceeqv 3567	. . . . . . . . 9 ⊢ ((◡𝑢 ∈ 𝑈 ∧ ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
130	121, 127, 129	syl2anc 583	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
131		elrest 17055	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))))
132	131	biimpar 477	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
133	87, 119, 130, 132	syl21anc 834	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
134	133, 55	r19.29a 3217	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
135		simp-4l 779	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑈 ∈ (UnifOn‘𝑋))
136	14	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝐴 × 𝐴) ∈ V)
137		simplr 765	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑥 ∈ 𝑈)
138		elrestr 17056	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑥 ∈ 𝑈) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
139	135, 136, 137, 138	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
140		inss1 4159	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥
141		coss1 5753	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))))
142		coss2 5754	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
143	141, 142	sstrd 3927	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
144	140, 143	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥)
145		sstr 3925	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
146	144, 145	mpan 686	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘ 𝑥) ⊆ 𝑢 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
147	146	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
148		inss2 4160	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
149		coss1 5753	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
150		coss2 5754	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
151	149, 150	sstrd 3927	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
152	148, 151	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))
153		xpidtr 6016	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
154	152, 153	sstri 3926	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)
155	154	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))
156	147, 155	ssind 4163	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
157		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
158	157, 157	coeq12d 5762	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → (𝑤 ∘ 𝑤) = ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
159	158	sseq1d 3948	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → ((𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)) ↔ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
160	159	rspcev 3552	. . . . . . . . . . 11 ⊢ (((𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
161	139, 156, 160	syl2anc 583	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
162		ustexhalf 23270	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
163	162	adantlr 711	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
164	161, 163	r19.29a 3217	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
165	164	ad4ant13 747	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
166	116	sseq2d 3949	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ (𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
167	166	rexbidv 3225	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
168	165, 167	mpbird 256	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
169	168, 55	r19.29a 3217	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
170	118, 134, 169	3jca 1126	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))
171	59, 86, 170	3jca 1126	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
172	171	ralrimiva 3107	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
173	2, 19, 172	3jca 1126	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))))
174		isust 23263	. . 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 256	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4530   class class class wbr 5070   I cid 5479   × cxp 5578  ^◡ccnv 5579  dom cdm 5580   ↾ cres 5582   ∘ ccom 5584  ‘cfv 6418  (class class class)co 7255   ↾_t crest 17048  UnifOncust 23259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-rest 17050  df-ust 23260

This theorem is referenced by:  restutop  23297  restutopopn  23298  ressust  23323  ressusp  23324  trcfilu  23354  cfiluweak  23355