Theorem trust 23381

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 17142	. . . 4 ⊢ (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴)
2	1	a1i 11	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴))
3		inxp 5741	. . . . . 6 ⊢ ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴))
4		sseqin2 4149	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
5	4	biimpi 215	. . . . . . 7 ⊢ (𝐴 ⊆ 𝑋 → (𝑋 ∩ 𝐴) = 𝐴)
6	5	sqxpeqd 5621	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴)) = (𝐴 × 𝐴))
7	3, 6	eqtrid 2790	. . . . 5 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
8	7	adantl 482	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
9		simpl 483	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
10		elfvex 6807	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
11	10	adantr 481	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
12		simpr 485	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
13	11, 12	ssexd 5248	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	13, 13	xpexd 7601	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ V)
15		ustbasel 23358	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
16	15	adantr 481	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
17		elrestr 17139	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ (𝑋 × 𝑋) ∈ 𝑈) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
18	9, 14, 16, 17	syl3anc 1370	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
19	8, 18	eqeltrrd 2840	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
20	9	ad5antr 731	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
21	14	ad5antr 731	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
22		simplr 766	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
23		simp-4r 781	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ 𝒫 (𝐴 × 𝐴))
24	23	elpwid 4544	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝐴 × 𝐴))
25	12	ad5antr 731	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
26		xpss12 5604	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
27	25, 25, 26	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
28	24, 27	sstrd 3931	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝑋 × 𝑋))
29		ustssxp 23356	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → 𝑢 ⊆ (𝑋 × 𝑋))
30	20, 22, 29	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ⊆ (𝑋 × 𝑋))
31	28, 30	unssd 4120	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋))
32		ssun2 4107	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑤 ∪ 𝑢)
33		ustssel 23357	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑢 ⊆ (𝑤 ∪ 𝑢) → (𝑤 ∪ 𝑢) ∈ 𝑈))
34	32, 33	mpi 20	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑤 ∪ 𝑢) ∈ 𝑈)
35	20, 22, 31, 34	syl3anc 1370	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ∈ 𝑈)
36		df-ss 3904	. . . . . . . . . . . . . 14 ⊢ (𝑤 ⊆ (𝐴 × 𝐴) ↔ (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
37	24, 36	sylib 217	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
38	37	uneq1d 4096	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))) = (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))))
39		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
40		simpllr 773	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 ⊆ 𝑤)
41	39, 40	eqsstrrd 3960	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤)
42		ssequn2 4117	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤 ↔ (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
43	41, 42	sylib 217	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
44	38, 43	eqtr2d 2779	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))))
45		indir 4209	. . . . . . . . . . 11 ⊢ ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)) = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴)))
46	44, 45	eqtr4di 2796	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
47		ineq1 4139	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑤 ∪ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
48	47	rspceeqv 3575	. . . . . . . . . 10 ⊢ (((𝑤 ∪ 𝑢) ∈ 𝑈 ∧ 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
49	35, 46, 48	syl2anc 584	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
50		elrest 17138	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
51	50	biimpar 478	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
52	20, 21, 49, 51	syl21anc 835	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
53		elrest 17138	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))))
54	53	biimpa 477	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
55	14, 54	syldanl 602	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
56	55	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
57	52, 56	r19.29a 3218	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
58	57	ex 413	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) → (𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
59	58	ralrimiva 3103	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
60	9	ad5antr 731	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑈 ∈ (UnifOn‘𝑋))
61	14	ad5antr 731	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝐴 × 𝐴) ∈ V)
62		simpllr 773	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑢 ∈ 𝑈)
63		simplr 766	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑥 ∈ 𝑈)
64		ustincl 23359	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) → (𝑢 ∩ 𝑥) ∈ 𝑈)
65	60, 62, 63, 64	syl3anc 1370	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑢 ∩ 𝑥) ∈ 𝑈)
66		simprl 768	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
67		simprr 770	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
68	66, 67	ineq12d 4147	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴))))
69		inindir 4161	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴)))
70	68, 69	eqtr4di 2796	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
71		ineq1 4139	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑥) → (𝑦 ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
72	71	rspceeqv 3575	. . . . . . . . 9 ⊢ (((𝑢 ∩ 𝑥) ∈ 𝑈 ∧ (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
73	65, 70, 72	syl2anc 584	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
74		elrest 17138	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → ((𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))))
75	74	biimpar 478	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
76	60, 61, 73, 75	syl21anc 835	. . . . . . 7 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
77	55	adantr 481	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
78	9	ad2antrr 723	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
79	14	ad2antrr 723	. . . . . . . . 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 835	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
83		reeanv 3294	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) ↔ (∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
84	77, 82, 83	sylanbrc 583	. . . . . . 7 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
85	76, 84	r19.29vva 3266	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
86	85	ralrimiva 3103	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
87		simp-4l 780	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
88		simplr 766	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
89		ustdiag 23360	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑢)
90	87, 88, 89	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝑋) ⊆ 𝑢)
91		simp-4r 781	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
92		inss1 4162	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ ( I ↾ 𝑋)
93		resss 5916	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝑋) ⊆ I
94	92, 93	sstri 3930	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I
95		iss 5943	. . . . . . . . . . . . 13 ⊢ ((( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I ↔ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))))
96	94, 95	mpbi 229	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
97		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
98		ssel2 3916	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝑋)
99		equid 2015	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑢 = 𝑢
100		resieq 5902	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑢( I ↾ 𝑋)𝑢 ↔ 𝑢 = 𝑢))
101	99, 100	mpbiri 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → 𝑢( I ↾ 𝑋)𝑢)
102	98, 98, 101	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢( I ↾ 𝑋)𝑢)
103		breq2 5078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑢 → (𝑢( I ↾ 𝑋)𝑣 ↔ 𝑢( I ↾ 𝑋)𝑢))
104	103	rspcev 3561	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑢( I ↾ 𝑋)𝑢) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
105	97, 102, 104	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
106	105	ralrimiva 3103	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝑋 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
107		dminxp 6083	. . . . . . . . . . . . . 14 ⊢ (dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
108	106, 107	sylibr 233	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑋 → dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴)
109	108	reseq2d 5891	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))) = ( I ↾ 𝐴))
110	96, 109	eqtr2id 2791	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
111	110	adantl 482	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
112		ssrin 4167	. . . . . . . . . . 11 ⊢ (( I ↾ 𝑋) ⊆ 𝑢 → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
113	112	adantr 481	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
114	111, 113	eqsstrd 3959	. . . . . . . . 9 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
115	90, 91, 114	syl2anc 584	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
116		simpr 485	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
117	115, 116	sseqtrrd 3962	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
118	117, 55	r19.29a 3218	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
119	14	ad3antrrr 727	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
120		ustinvel 23361	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ◡𝑢 ∈ 𝑈)
121	87, 88, 120	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑢 ∈ 𝑈)
122	116	cnveqd 5784	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = ◡(𝑢 ∩ (𝐴 × 𝐴)))
123		cnvin 6048	. . . . . . . . . . 11 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ ◡(𝐴 × 𝐴))
124		cnvxp 6060	. . . . . . . . . . . 12 ⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴)
125	124	ineq2i 4143	. . . . . . . . . . 11 ⊢ (◡𝑢 ∩ ◡(𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
126	123, 125	eqtri 2766	. . . . . . . . . 10 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
127	122, 126	eqtrdi 2794	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴)))
128		ineq1 4139	. . . . . . . . . 10 ⊢ (𝑥 = ◡𝑢 → (𝑥 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴)))
129	128	rspceeqv 3575	. . . . . . . . 9 ⊢ ((◡𝑢 ∈ 𝑈 ∧ ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
130	121, 127, 129	syl2anc 584	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
131		elrest 17138	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))))
132	131	biimpar 478	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
133	87, 119, 130, 132	syl21anc 835	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
134	133, 55	r19.29a 3218	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
135		simp-4l 780	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑈 ∈ (UnifOn‘𝑋))
136	14	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝐴 × 𝐴) ∈ V)
137		simplr 766	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑥 ∈ 𝑈)
138		elrestr 17139	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑥 ∈ 𝑈) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
139	135, 136, 137, 138	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
140		inss1 4162	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥
141		coss1 5764	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))))
142		coss2 5765	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
143	141, 142	sstrd 3931	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
144	140, 143	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥)
145		sstr 3929	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
146	144, 145	mpan 687	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘ 𝑥) ⊆ 𝑢 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
147	146	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
148		inss2 4163	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
149		coss1 5764	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
150		coss2 5765	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
151	149, 150	sstrd 3931	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
152	148, 151	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))
153		xpidtr 6027	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
154	152, 153	sstri 3930	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)
155	154	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))
156	147, 155	ssind 4166	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
157		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
158	157, 157	coeq12d 5773	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → (𝑤 ∘ 𝑤) = ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
159	158	sseq1d 3952	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → ((𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)) ↔ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
160	159	rspcev 3561	. . . . . . . . . . 11 ⊢ (((𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
161	139, 156, 160	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
162		ustexhalf 23362	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
163	162	adantlr 712	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
164	161, 163	r19.29a 3218	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
165	164	ad4ant13 748	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
166	116	sseq2d 3953	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ (𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
167	166	rexbidv 3226	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
168	165, 167	mpbird 256	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
169	168, 55	r19.29a 3218	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
170	118, 134, 169	3jca 1127	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))
171	59, 86, 170	3jca 1127	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
172	171	ralrimiva 3103	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
173	2, 19, 172	3jca 1127	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))))
174		isust 23355	. . 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 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  𝒫 cpw 4533   class class class wbr 5074   I cid 5488   × cxp 5587  ^◡ccnv 5588  dom cdm 5589   ↾ cres 5591   ∘ ccom 5593  ‘cfv 6433  (class class class)co 7275   ↾_t crest 17131  UnifOncust 23351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-rest 17133  df-ust 23352

This theorem is referenced by:  restutop  23389  restutopopn  23390  ressust  23415  ressusp  23416  trcfilu  23446  cfiluweak  23447