Theorem trust 24541

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 17595	. . . 4 ⊢ (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴)
2	1	a1i 11	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴))
3		inxp 5809	. . . . . 6 ⊢ ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴))
4		sseqin2 4169	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
5	4	biimpi 219	. . . . . . 7 ⊢ (𝐴 ⊆ 𝑋 → (𝑋 ∩ 𝐴) = 𝐴)
6	5	sqxpeqd 5683	. . . . . 6 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 ∩ 𝐴) × (𝑋 ∩ 𝐴)) = (𝐴 × 𝐴))
7	3, 6	eqtrid 2808	. . . . 5 ⊢ (𝐴 ⊆ 𝑋 → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
8	7	adantl 487	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
9		simpl 488	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
10		elfvex 6918	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
11	10	adantr 486	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
12		simpr 490	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
13	11, 12	ssexd 5286	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	13, 13	xpexd 7763	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ V)
15		ustbasel 24519	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
16	15	adantr 486	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
17		elrestr 17592	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ (𝑋 × 𝑋) ∈ 𝑈) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
18	9, 14, 16, 17	syl3anc 1398	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
19	8, 18	eqeltrrd 2862	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
20	9	ad5antr 747	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
21	14	ad5antr 747	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
22		simplr 781	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
23		simp-4r 796	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ 𝒫 (𝐴 × 𝐴))
24	23	elpwid 4566	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝐴 × 𝐴))
25	12	ad5antr 747	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
26		xpss12 5666	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
27	25, 25, 26	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
28	24, 27	sstrd 3941	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝑋 × 𝑋))
29		ustssxp 24517	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → 𝑢 ⊆ (𝑋 × 𝑋))
30	20, 22, 29	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ⊆ (𝑋 × 𝑋))
31	28, 30	unssd 4138	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋))
32		ssun2 4125	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑤 ∪ 𝑢)
33		ustssel 24518	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑢 ⊆ (𝑤 ∪ 𝑢) → (𝑤 ∪ 𝑢) ∈ 𝑈))
34	32, 33	mpi 21	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ (𝑤 ∪ 𝑢) ⊆ (𝑋 × 𝑋)) → (𝑤 ∪ 𝑢) ∈ 𝑈)
35	20, 22, 31, 34	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ 𝑢) ∈ 𝑈)
36		dfss2 3917	. . . . . . . . . . . . . 14 ⊢ (𝑤 ⊆ (𝐴 × 𝐴) ↔ (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
37	24, 36	sylib 221	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
38	37	uneq1d 4114	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))) = (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))))
39		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
40		simpllr 788	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 ⊆ 𝑤)
41	39, 40	eqsstrrd 3966	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤)
42		ssequn2 4135	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤 ↔ (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
43	41, 42	sylib 221	. . . . . . . . . . . 12 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
44	38, 43	eqtr2d 2797	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))))
45		indir 4232	. . . . . . . . . . 11 ⊢ ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)) = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴)))
46	44, 45	eqtr4di 2814	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
47		ineq1 4159	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑤 ∪ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴)))
48	47	rspceeqv 3599	. . . . . . . . . 10 ⊢ (((𝑤 ∪ 𝑢) ∈ 𝑈 ∧ 𝑤 = ((𝑤 ∪ 𝑢) ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
49	35, 46, 48	syl2anc 596	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
50		elrest 17591	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
51	50	biimpar 483	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
52	20, 21, 49, 51	syl21anc 851	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
53		elrest 17591	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))))
54	53	biimpa 482	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
55	14, 54	syldanl 614	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
56	55	ad2antrr 739	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
57	52, 56	r19.29a 3171	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣 ⊆ 𝑤) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
58	57	ex 418	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) → (𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
59	58	ralrimiva 3155	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))))
60	9	ad5antr 747	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑈 ∈ (UnifOn‘𝑋))
61	14	ad5antr 747	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝐴 × 𝐴) ∈ V)
62		simpllr 788	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑢 ∈ 𝑈)
63		simplr 781	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑥 ∈ 𝑈)
64		ustincl 24520	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) → (𝑢 ∩ 𝑥) ∈ 𝑈)
65	60, 62, 63, 64	syl3anc 1398	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑢 ∩ 𝑥) ∈ 𝑈)
66		simprl 783	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
67		simprr 785	. . . . . . . . . . 11 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
68	66, 67	ineq12d 4167	. . . . . . . . . 10 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴))))
69		inindir 4181	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴)))
70	68, 69	eqtr4di 2814	. . . . . . . . 9 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
71		ineq1 4159	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑥) → (𝑦 ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴)))
72	71	rspceeqv 3599	. . . . . . . . 9 ⊢ (((𝑢 ∩ 𝑥) ∈ 𝑈 ∧ (𝑣 ∩ 𝑤) = ((𝑢 ∩ 𝑥) ∩ (𝐴 × 𝐴))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
73	65, 70, 72	syl2anc 596	. . . . . . . 8 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
74		elrest 17591	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → ((𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))))
75	74	biimpar 483	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑦 ∈ 𝑈 (𝑣 ∩ 𝑤) = (𝑦 ∩ (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
76	60, 61, 73, 75	syl21anc 851	. . . . . . 7 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
77	55	adantr 486	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
78	9	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
79	14	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
80		simpr 490	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
81	50	biimpa 482	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
82	78, 79, 80, 81	syl21anc 851	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
83		reeanv 3235	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) ↔ (∃𝑢 ∈ 𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ ∃𝑥 ∈ 𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
84	77, 82, 83	sylanbrc 595	. . . . . . 7 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑢 ∈ 𝑈 ∃𝑥 ∈ 𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
85	76, 84	r19.29vva 3223	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
86	85	ralrimiva 3155	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
87		simp-4l 795	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
88		simplr 781	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝑈)
89		ustdiag 24521	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑢)
90	87, 88, 89	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝑋) ⊆ 𝑢)
91		simp-4r 796	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴 ⊆ 𝑋)
92		inss1 4182	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ ( I ↾ 𝑋)
93		resss 5992	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝑋) ⊆ I
94	92, 93	sstri 3940	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I
95		iss 6027	. . . . . . . . . . . . 13 ⊢ ((( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I ↔ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))))
96	94, 95	mpbi 233	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
97		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴)
98		ssel2 3926	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝑋)
99		equid 2045	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑢 = 𝑢
100		resieq 5981	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑢( I ↾ 𝑋)𝑢 ↔ 𝑢 = 𝑢))
101	99, 100	mpbiri 261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → 𝑢( I ↾ 𝑋)𝑢)
102	98, 98, 101	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → 𝑢( I ↾ 𝑋)𝑢)
103		breq2 5107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑢 → (𝑢( I ↾ 𝑋)𝑣 ↔ 𝑢( I ↾ 𝑋)𝑢))
104	103	rspcev 3577	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑢( I ↾ 𝑋)𝑢) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
105	97, 102, 104	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑢 ∈ 𝐴) → ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
106	105	ralrimiva 3155	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝑋 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
107		dminxp 6172	. . . . . . . . . . . . . 14 ⊢ (dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 𝑢( I ↾ 𝑋)𝑣)
108	106, 107	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑋 → dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴)
109	108	reseq2d 5970	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))) = ( I ↾ 𝐴))
110	96, 109	eqtr2id 2809	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝑋 → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
111	110	adantl 487	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
112		ssrin 4187	. . . . . . . . . . 11 ⊢ (( I ↾ 𝑋) ⊆ 𝑢 → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
113	112	adantr 486	. . . . . . . . . 10 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
114	111, 113	eqsstrd 3965	. . . . . . . . 9 ⊢ ((( I ↾ 𝑋) ⊆ 𝑢 ∧ 𝐴 ⊆ 𝑋) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
115	90, 91, 114	syl2anc 596	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
116		simpr 490	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
117	115, 116	sseqtrrd 3968	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
118	117, 55	r19.29a 3171	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
119	14	ad3antrrr 743	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
120		ustinvel 24522	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ◡𝑢 ∈ 𝑈)
121	87, 88, 120	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑢 ∈ 𝑈)
122	116	cnveqd 5853	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = ◡(𝑢 ∩ (𝐴 × 𝐴)))
123		cnvin 6135	. . . . . . . . . . 11 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ ◡(𝐴 × 𝐴))
124		cnvxp 6147	. . . . . . . . . . . 12 ⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴)
125	124	ineq2i 4163	. . . . . . . . . . 11 ⊢ (◡𝑢 ∩ ◡(𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
126	123, 125	eqtri 2784	. . . . . . . . . 10 ⊢ ◡(𝑢 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴))
127	122, 126	eqtrdi 2812	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴)))
128		ineq1 4159	. . . . . . . . . 10 ⊢ (𝑥 = ◡𝑢 → (𝑥 ∩ (𝐴 × 𝐴)) = (◡𝑢 ∩ (𝐴 × 𝐴)))
129	128	rspceeqv 3599	. . . . . . . . 9 ⊢ ((◡𝑢 ∈ 𝑈 ∧ ◡𝑣 = (◡𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
130	121, 127, 129	syl2anc 596	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
131		elrest 17591	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))))
132	131	biimpar 483	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥 ∈ 𝑈 ◡𝑣 = (𝑥 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
133	87, 119, 130, 132	syl21anc 851	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
134	133, 55	r19.29a 3171	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)))
135		simp-4l 795	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑈 ∈ (UnifOn‘𝑋))
136	14	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝐴 × 𝐴) ∈ V)
137		simplr 781	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → 𝑥 ∈ 𝑈)
138		elrestr 17592	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑥 ∈ 𝑈) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
139	135, 136, 137, 138	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
140		inss1 4182	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥
141		coss1 5833	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))))
142		coss2 5834	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
143	141, 142	sstrd 3941	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥))
144	140, 143	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥)
145		sstr 3939	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ 𝑥) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
146	144, 145	mpan 703	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘ 𝑥) ⊆ 𝑢 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
147	146	adantl 487	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
148		inss2 4183	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
149		coss1 5833	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
150		coss2 5834	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
151	149, 150	sstrd 3941	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
152	148, 151	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))
153		xpidtr 6116	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
154	152, 153	sstri 3940	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)
155	154	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))
156	147, 155	ssind 4186	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
157		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
158	157, 157	coeq12d 5842	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → (𝑤 ∘ 𝑤) = ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
159	158	sseq1d 3962	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → ((𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)) ↔ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
160	159	rspcev 3577	. . . . . . . . . . 11 ⊢ (((𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
161	139, 156, 160	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) ∧ 𝑥 ∈ 𝑈) ∧ (𝑥 ∘ 𝑥) ⊆ 𝑢) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
162		ustexhalf 24523	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
163	162	adantlr 728	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 (𝑥 ∘ 𝑥) ⊆ 𝑢)
164	161, 163	r19.29a 3171	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
165	164	ad4ant13 764	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
166	116	sseq2d 3963	. . . . . . . . 9 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ (𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
167	166	rexbidv 3187	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
168	165, 167	mpbird 260	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
169	168, 55	r19.29a 3171	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)
170	118, 134, 169	3jca 1146	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))
171	59, 86, 170	3jca 1146	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → (∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
172	171	ralrimiva 3155	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))
173	2, 19, 172	3jca 1146	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣))))
174		isust 24516	. . 3 ⊢ (𝐴 ∈ V → ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) ↔ ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))))
175	13, 174	syl 18	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) ↔ ((𝑈 ↾t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣 ⊆ 𝑤 → 𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 ∩ 𝑤) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣 ∧ ◡𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑤 ∘ 𝑤) ⊆ 𝑣)))))
176	173, 175	mpbird 260	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557   class class class wbr 5103   I cid 5545   × cxp 5649  ^◡ccnv 5650  dom cdm 5651   ↾ cres 5653   ∘ ccom 5655  ‘cfv 6537  (class class class)co 7418   ↾_t crest 17584  UnifOncust 24512

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-1st 7999  df-2nd 8000  df-rest 17586  df-ust 24513

This theorem is used by:  restutop  24549  restutopopn  24550  ressust  24575  ressusp  24576  trcfilu  24605  cfiluweak  24606