Theorem trust 24219

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 17392	. . . 4 ⊢ (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴)
2	1	a1i 11	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴))
3		inxp 5781	. . . . . 6 ⊢ ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴))
4		sseqin2 4159	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
5	4	biimpi 217	. . . . . . 7 ⊢ (𝐴 ⊆ 𝑋 → (𝑋 ∩ 𝐴) = 𝐴)
6	5	sqxpeqd 5657	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴)) = (𝐴 × 𝐴))
7	3, 6	eqtrid 2787	. . . . 5 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
8	7	adantl 482	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
9		simpl 483	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
10		elfvex 6869	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
11	10	adantr 481	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
12		simpr 485	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
13	11, 12	ssexd 5259	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	13, 13	xpexd 7701	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ V)
15		ustbasel 24197	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
16	15	adantr 481	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
17		elrestr 17389	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ (𝑋 × 𝑋) ∈ 𝑈) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
18	9, 14, 16, 17	syl3anc 1379	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
19	8, 18	eqeltrrd 2841	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
20	9	ad5antr 740	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
21	14	ad5antr 740	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
22		simplr 774	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
23		simp-4r 789	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ 𝒫 (𝐴 × 𝐴))
24	23	elpwid 4545	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝐴 × 𝐴))
25	12	ad5antr 740	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
26		xpss12 5640	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
27	25, 25, 26	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
28	24, 27	sstrd 3932	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝑋 × 𝑋))
29		ustssxp 24195	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → 𝑢 ⊆ (𝑋 × 𝑋))
30	20, 22, 29	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ⊆ (𝑋 × 𝑋))
31	28, 30	unssd 4128	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋))
32		ssun2 4115	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑤 ∪ 𝑢)
33		ustssel 24196	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑢 ⊆ (𝑤 ∪ 𝑢) → (𝑤 ∪ 𝑢) ∈ 𝑈))
34	32, 33	mpi 20	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑤 ∪ 𝑢) ∈ 𝑈)
35	20, 22, 31, 34	syl3anc 1379	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ∈ 𝑈)
36		dfss2 3908	. . . . . . . . . . . . . 14 ⊢ (𝑤 ⊆ (𝐴 × 𝐴) ↔ (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
37	24, 36	sylib 219	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
38	37	uneq1d 4104	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))) = (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))))
39		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
40		simpllr 781	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 ⊆ 𝑤)
41	39, 40	eqsstrrd 3957	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤)
42		ssequn2 4125	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤 ↔ (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
43	41, 42	sylib 219	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
44	38, 43	eqtr2d 2776	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))))
45		indir 4221	. . . . . . . . . . 11 ⊢ ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)) = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴)))
46	44, 45	eqtr4di 2793	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
47		ineq1 4149	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑤 ∪ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
48	47	rspceeqv 3590	. . . . . . . . . 10 ⊢ (((𝑤 ∪ 𝑢) ∈ 𝑈 ∧ 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
49	35, 46, 48	syl2anc 590	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
50		elrest 17388	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
51	50	biimpar 478	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
52	20, 21, 49, 51	syl21anc 843	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
53		elrest 17388	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))))
54	53	biimpa 477	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
55	14, 54	syldanl 608	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
56	55	ad2antrr 732	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
57	52, 56	r19.29a 3148	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
58	57	ex 413	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) → (𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
59	58	ralrimiva 3132	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
60	9	ad5antr 740	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑈 ∈ (UnifOn‘𝑋))
61	14	ad5antr 740	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝐴 × 𝐴) ∈ V)
62		simpllr 781	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑢 ∈ 𝑈)
63		simplr 774	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑥 ∈ 𝑈)
64		ustincl 24198	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) → (𝑢 ∩ 𝑥) ∈ 𝑈)
65	60, 62, 63, 64	syl3anc 1379	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑢 ∩ 𝑥) ∈ 𝑈)
66		simprl 776	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
67		simprr 778	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
68	66, 67	ineq12d 4157	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴))))
69		inindir 4171	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴)))
70	68, 69	eqtr4di 2793	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
71		ineq1 4149	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑥) → (𝑦 ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
72	71	rspceeqv 3590	. . . . . . . . 9 ⊢ (((𝑢 ∩ 𝑥) ∈ 𝑈 ∧ (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
73	65, 70, 72	syl2anc 590	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
74		elrest 17388	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → ((𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))))
75	74	biimpar 478	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
76	60, 61, 73, 75	syl21anc 843	. . . . . . 7 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
77	55	adantr 481	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
78	9	ad2antrr 732	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
79	14	ad2antrr 732	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
80		simpr 485	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
81	50	biimpa 477	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
82	78, 79, 80, 81	syl21anc 843	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
83		reeanv 3212	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) ↔ (∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
84	77, 82, 83	sylanbrc 589	. . . . . . 7 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
85	76, 84	r19.29vva 3200	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
86	85	ralrimiva 3132	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
87		simp-4l 788	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
88		simplr 774	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
89		ustdiag 24199	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑢)
90	87, 88, 89	syl2anc 590	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝑋) ⊆ 𝑢)
91		simp-4r 789	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
92		inss1 4172	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ ( I ↾ 𝑋)
93		resss 5960	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝑋) ⊆ I
94	92, 93	sstri 3931	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I
95		iss 5994	. . . . . . . . . . . . 13 ⊢ ((( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I ↔ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))))
96	94, 95	mpbi 231	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
97		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
98		ssel2 3917	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝑋)
99		equid 2019	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑢 = 𝑢
100		resieq 5949	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑢( I ↾ 𝑋)𝑢 ↔ 𝑢 = 𝑢))
101	99, 100	mpbiri 259	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → 𝑢( I ↾ 𝑋)𝑢)
102	98, 98, 101	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢( I ↾ 𝑋)𝑢)
103		breq2 5083	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑢 → (𝑢( I ↾ 𝑋)𝑣 ↔ 𝑢( I ↾ 𝑋)𝑢))
104	103	rspcev 3567	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑢( I ↾ 𝑋)𝑢) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
105	97, 102, 104	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
106	105	ralrimiva 3132	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝑋 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
107		dminxp 6138	. . . . . . . . . . . . . 14 ⊢ (dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
108	106, 107	sylibr 235	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑋 → dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴)
109	108	reseq2d 5938	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))) = ( I ↾ 𝐴))
110	96, 109	eqtr2id 2788	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
111	110	adantl 482	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
112		ssrin 4177	. . . . . . . . . . 11 ⊢ (( I ↾ 𝑋) ⊆ 𝑢 → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
113	112	adantr 481	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
114	111, 113	eqsstrd 3956	. . . . . . . . 9 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
115	90, 91, 114	syl2anc 590	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
116		simpr 485	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
117	115, 116	sseqtrrd 3959	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
118	117, 55	r19.29a 3148	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
119	14	ad3antrrr 736	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
120		ustinvel 24200	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ◡𝑢 ∈ 𝑈)
121	87, 88, 120	syl2anc 590	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑢 ∈ 𝑈)
122	116	cnveqd 5824	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = ◡(𝑢 ∩ (𝐴 × 𝐴)))
123		cnvin 6102	. . . . . . . . . . 11 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ ◡(𝐴 × 𝐴))
124		cnvxp 6115	. . . . . . . . . . . 12 ⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴)
125	124	ineq2i 4153	. . . . . . . . . . 11 ⊢ (◡𝑢 ∩ ◡(𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
126	123, 125	eqtri 2763	. . . . . . . . . 10 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
127	122, 126	eqtrdi 2791	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴)))
128		ineq1 4149	. . . . . . . . . 10 ⊢ (𝑥 = ◡𝑢 → (𝑥 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴)))
129	128	rspceeqv 3590	. . . . . . . . 9 ⊢ ((◡𝑢 ∈ 𝑈 ∧ ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
130	121, 127, 129	syl2anc 590	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
131		elrest 17388	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))))
132	131	biimpar 478	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
133	87, 119, 130, 132	syl21anc 843	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
134	133, 55	r19.29a 3148	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
135		simp-4l 788	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑈 ∈ (UnifOn‘𝑋))
136	14	ad3antrrr 736	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝐴 × 𝐴) ∈ V)
137		simplr 774	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑥 ∈ 𝑈)
138		elrestr 17389	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑥 ∈ 𝑈) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
139	135, 136, 137, 138	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
140		inss1 4172	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥
141		coss1 5804	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))))
142		coss2 5805	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
143	141, 142	sstrd 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
144	140, 143	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥)
145		sstr 3930	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
146	144, 145	mpan 696	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘ 𝑥) ⊆ 𝑢 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
147	146	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
148		inss2 4173	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
149		coss1 5804	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
150		coss2 5805	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
151	149, 150	sstrd 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
152	148, 151	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))
153		xpidtr 6079	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
154	152, 153	sstri 3931	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)
155	154	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))
156	147, 155	ssind 4176	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
157		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
158	157, 157	coeq12d 5813	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → (𝑤 ∘ 𝑤) = ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
159	158	sseq1d 3953	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → ((𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)) ↔ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
160	159	rspcev 3567	. . . . . . . . . . 11 ⊢ (((𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
161	139, 156, 160	syl2anc 590	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
162		ustexhalf 24201	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
163	162	adantlr 721	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
164	161, 163	r19.29a 3148	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
165	164	ad4ant13 757	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
166	116	sseq2d 3954	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ (𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
167	166	rexbidv 3164	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
168	165, 167	mpbird 258	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
169	168, 55	r19.29a 3148	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
170	118, 134, 169	3jca 1134	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))
171	59, 86, 170	3jca 1134	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
172	171	ralrimiva 3132	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
173	2, 19, 172	3jca 1134	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))))
174		isust 24194	. . 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 258	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064  Vcvv 3432   ∪ cun 3888   ∩ cin 3889   ⊆ wss 3890  𝒫 cpw 4536   class class class wbr 5079   I cid 5519   × cxp 5623  ^◡ccnv 5624  dom cdm 5625   ↾ cres 5627   ∘ ccom 5629  ‘cfv 6492  (class class class)co 7363   ↾_t crest 17381  UnifOncust 24190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-rest 17383  df-ust 24191

This theorem is referenced by:  restutop  24227  restutopopn  24228  ressust  24253  ressusp  24254  trcfilu  24283  cfiluweak  24284