trust

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

		Ref	Expression
	Assertion	trust	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$

Proof

Step	Hyp	Ref	Expression
1		restsspw	$⊢ U ↾_{𝑡} (A \times A) \subseteq 𝒫 (A \times A)$
2	1	a1i	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \subseteq 𝒫 (A \times A)$
3		inxp	$⊢ (X \times X) \cap (A \times A) = (X \cap A) \times (X \cap A)$
4		sseqin2	$⊢ A \subseteq X \leftrightarrow X \cap A = A$
5	4	biimpi	$⊢ A \subseteq X \to X \cap A = A$
6	5	sqxpeqd	$⊢ A \subseteq X \to (X \cap A) \times (X \cap A) = A \times A$
7	3 6	eqtrid	$⊢ A \subseteq X \to (X \times X) \cap (A \times A) = A \times A$
8	7	adantl	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to (X \times X) \cap (A \times A) = A \times A$
9		simpl	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U \in UnifOn (X)$
10		elfvex	$⊢ U \in UnifOn (X) \to X \in V$
11	10	adantr	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to X \in V$
12		simpr	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to A \subseteq X$
13	11 12	ssexd	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to A \in V$
14	13 13	xpexd	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to A \times A \in V$
15		ustbasel	$⊢ U \in UnifOn (X) \to X \times X \in U$
16	15	adantr	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to X \times X \in U$
17		elrestr	$⊢ (U \in UnifOn (X) \land A \times A \in V \land X \times X \in U) \to (X \times X) \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
18	9 14 16 17	syl3anc	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to (X \times X) \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
19	8 18	eqeltrrd	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to A \times A \in (U ↾_{𝑡} (A \times A))$
20	9	ad5antr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to U \in UnifOn (X)$
21	14	ad5antr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to A \times A \in V$
22		simplr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to u \in U$
23		simp-4r	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \in 𝒫 (A \times A)$
24	23	elpwid	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \subseteq A \times A$
25	12	ad5antr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to A \subseteq X$
26		xpss12	$⊢ (A \subseteq X \land A \subseteq X) \to A \times A \subseteq X \times X$
27	25 25 26	syl2anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to A \times A \subseteq X \times X$
28	24 27	sstrd	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \subseteq X \times X$
29		ustssxp	$⊢ (U \in UnifOn (X) \land u \in U) \to u \subseteq X \times X$
30	20 22 29	syl2anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to u \subseteq X \times X$
31	28 30	unssd	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \cup u \subseteq X \times X$
32		ssun2	$⊢ u \subseteq w \cup u$
33		ustssel	$⊢ (U \in UnifOn (X) \land u \in U \land w \cup u \subseteq X \times X) \to (u \subseteq w \cup u \to w \cup u \in U)$
34	32 33	mpi	$⊢ (U \in UnifOn (X) \land u \in U \land w \cup u \subseteq X \times X) \to w \cup u \in U$
35	20 22 31 34	syl3anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \cup u \in U$
36		df-ss	$⊢ w \subseteq A \times A \leftrightarrow w \cap (A \times A) = w$
37	24 36	sylib	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \cap (A \times A) = w$
38	37	uneq1d	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to (w \cap (A \times A)) \cup (u \cap (A \times A)) = w \cup (u \cap (A \times A))$
39		simpr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to v = u \cap (A \times A)$
40		simpllr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to v \subseteq w$
41	39 40	eqsstrrd	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to u \cap (A \times A) \subseteq w$
42		ssequn2	$⊢ u \cap (A \times A) \subseteq w \leftrightarrow w \cup (u \cap (A \times A)) = w$
43	41 42	sylib	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \cup (u \cap (A \times A)) = w$
44	38 43	eqtr2d	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w = (w \cap (A \times A)) \cup (u \cap (A \times A))$
45		indir	$⊢ (w \cup u) \cap (A \times A) = (w \cap (A \times A)) \cup (u \cap (A \times A))$
46	44 45	eqtr4di	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w = (w \cup u) \cap (A \times A)$
47		ineq1	$⊢ x = w \cup u \to x \cap (A \times A) = (w \cup u) \cap (A \times A)$
48	47	rspceeqv	$⊢ (w \cup u \in U \land w = (w \cup u) \cap (A \times A)) \to \exists x \in U w = x \cap (A \times A)$
49	35 46 48	syl2anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to \exists x \in U w = x \cap (A \times A)$
50		elrest	$⊢ (U \in UnifOn (X) \land A \times A \in V) \to (w \in (U ↾_{𝑡} (A \times A)) \leftrightarrow \exists x \in U w = x \cap (A \times A))$
51	50	biimpar	$⊢ ((U \in UnifOn (X) \land A \times A \in V) \land \exists x \in U w = x \cap (A \times A)) \to w \in (U ↾_{𝑡} (A \times A))$
52	20 21 49 51	syl21anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \land u \in U) \land v = u \cap (A \times A)) \to w \in (U ↾_{𝑡} (A \times A))$
53		elrest	$⊢ (U \in UnifOn (X) \land A \times A \in V) \to (v \in (U ↾_{𝑡} (A \times A)) \leftrightarrow \exists u \in U v = u \cap (A \times A))$
54	53	biimpa	$⊢ ((U \in UnifOn (X) \land A \times A \in V) \land v \in (U ↾_{𝑡} (A \times A))) \to \exists u \in U v = u \cap (A \times A)$
55	14 54	syldanl	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to \exists u \in U v = u \cap (A \times A)$
56	55	ad2antrr	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \to \exists u \in U v = u \cap (A \times A)$
57	52 56	r19.29a	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \land v \subseteq w) \to w \in (U ↾_{𝑡} (A \times A))$
58	57	ex	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in 𝒫 (A \times A)) \to (v \subseteq w \to w \in (U ↾_{𝑡} (A \times A)))$
59	58	ralrimiva	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to \forall w \in 𝒫 (A \times A) (v \subseteq w \to w \in (U ↾_{𝑡} (A \times A)))$
60	9	ad5antr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to U \in UnifOn (X)$
61	14	ad5antr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to A \times A \in V$
62		simpllr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to u \in U$
63		simplr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to x \in U$
64		ustincl	$⊢ (U \in UnifOn (X) \land u \in U \land x \in U) \to u \cap x \in U$
65	60 62 63 64	syl3anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to u \cap x \in U$
66		simprl	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to v = u \cap (A \times A)$
67		simprr	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to w = x \cap (A \times A)$
68	66 67	ineq12d	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to v \cap w = (u \cap (A \times A)) \cap (x \cap (A \times A))$
69		inindir	$⊢ (u \cap x) \cap (A \times A) = (u \cap (A \times A)) \cap (x \cap (A \times A))$
70	68 69	eqtr4di	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to v \cap w = (u \cap x) \cap (A \times A)$
71		ineq1	$⊢ y = u \cap x \to y \cap (A \times A) = (u \cap x) \cap (A \times A)$
72	71	rspceeqv	$⊢ (u \cap x \in U \land v \cap w = (u \cap x) \cap (A \times A)) \to \exists y \in U v \cap w = y \cap (A \times A)$
73	65 70 72	syl2anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to \exists y \in U v \cap w = y \cap (A \times A)$
74		elrest	$⊢ (U \in UnifOn (X) \land A \times A \in V) \to (v \cap w \in (U ↾_{𝑡} (A \times A)) \leftrightarrow \exists y \in U v \cap w = y \cap (A \times A))$
75	74	biimpar	$⊢ ((U \in UnifOn (X) \land A \times A \in V) \land \exists y \in U v \cap w = y \cap (A \times A)) \to v \cap w \in (U ↾_{𝑡} (A \times A))$
76	60 61 73 75	syl21anc	$⊢ ((((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land x \in U) \land (v = u \cap (A \times A) \land w = x \cap (A \times A))) \to v \cap w \in (U ↾_{𝑡} (A \times A))$
77	55	adantr	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \to \exists u \in U v = u \cap (A \times A)$
78	9	ad2antrr	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \to U \in UnifOn (X)$
79	14	ad2antrr	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \to A \times A \in V$
80		simpr	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \to w \in (U ↾_{𝑡} (A \times A))$
81	50	biimpa	$⊢ ((U \in UnifOn (X) \land A \times A \in V) \land w \in (U ↾_{𝑡} (A \times A))) \to \exists x \in U w = x \cap (A \times A)$
82	78 79 80 81	syl21anc	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \to \exists x \in U w = x \cap (A \times A)$
83		reeanv	$⊢ \exists u \in U \exists x \in U (v = u \cap (A \times A) \land w = x \cap (A \times A)) \leftrightarrow (\exists u \in U v = u \cap (A \times A) \land \exists x \in U w = x \cap (A \times A))$
84	77 82 83	sylanbrc	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \to \exists u \in U \exists x \in U (v = u \cap (A \times A) \land w = x \cap (A \times A))$
85	76 84	r19.29vva	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land w \in (U ↾_{𝑡} (A \times A))) \to v \cap w \in (U ↾_{𝑡} (A \times A))$
86	85	ralrimiva	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to \forall w \in (U ↾_{𝑡} (A \times A)) v \cap w \in (U ↾_{𝑡} (A \times A))$
87		simp-4l	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to U \in UnifOn (X)$
88		simplr	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to u \in U$
89		ustdiag	$⊢ (U \in UnifOn (X) \land u \in U) \to {I ↾}_{X} \subseteq u$
90	87 88 89	syl2anc	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to {I ↾}_{X} \subseteq u$
91		simp-4r	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to A \subseteq X$
92		inss1	$⊢ ({I ↾}_{X}) \cap (A \times A) \subseteq {I ↾}_{X}$
93		resss	$⊢ {I ↾}_{X} \subseteq I$
94	92 93	sstri	$⊢ ({I ↾}_{X}) \cap (A \times A) \subseteq I$
95		iss	$⊢ ({I ↾}_{X}) \cap (A \times A) \subseteq I \leftrightarrow ({I ↾}_{X}) \cap (A \times A) = {I ↾}_{dom (({I ↾}_{X}) \cap (A \times A))}$
96	94 95	mpbi	$⊢ ({I ↾}_{X}) \cap (A \times A) = {I ↾}_{dom (({I ↾}_{X}) \cap (A \times A))}$
97		simpr	$⊢ (A \subseteq X \land u \in A) \to u \in A$
98		ssel2	$⊢ (A \subseteq X \land u \in A) \to u \in X$
99		equid	$⊢ u = u$
100		resieq	$⊢ (u \in X \land u \in X) \to (u ({I ↾}_{X}) u \leftrightarrow u = u)$
101	99 100	mpbiri	$⊢ (u \in X \land u \in X) \to u ({I ↾}_{X}) u$
102	98 98 101	syl2anc	$⊢ (A \subseteq X \land u \in A) \to u ({I ↾}_{X}) u$
103		breq2	$⊢ v = u \to (u ({I ↾}_{X}) v \leftrightarrow u ({I ↾}_{X}) u)$
104	103	rspcev	$⊢ (u \in A \land u ({I ↾}_{X}) u) \to \exists v \in A u ({I ↾}_{X}) v$
105	97 102 104	syl2anc	$⊢ (A \subseteq X \land u \in A) \to \exists v \in A u ({I ↾}_{X}) v$
106	105	ralrimiva	$⊢ A \subseteq X \to \forall u \in A \exists v \in A u ({I ↾}_{X}) v$
107		dminxp	$⊢ dom (({I ↾}_{X}) \cap (A \times A)) = A \leftrightarrow \forall u \in A \exists v \in A u ({I ↾}_{X}) v$
108	106 107	sylibr	$⊢ A \subseteq X \to dom (({I ↾}_{X}) \cap (A \times A)) = A$
109	108	reseq2d	$⊢ A \subseteq X \to {I ↾}_{dom (({I ↾}_{X}) \cap (A \times A))} = {I ↾}_{A}$
110	96 109	eqtr2id	$⊢ A \subseteq X \to {I ↾}_{A} = ({I ↾}_{X}) \cap (A \times A)$
111	110	adantl	$⊢ ({I ↾}_{X} \subseteq u \land A \subseteq X) \to {I ↾}_{A} = ({I ↾}_{X}) \cap (A \times A)$
112		ssrin	$⊢ {I ↾}_{X} \subseteq u \to ({I ↾}_{X}) \cap (A \times A) \subseteq u \cap (A \times A)$
113	112	adantr	$⊢ ({I ↾}_{X} \subseteq u \land A \subseteq X) \to ({I ↾}_{X}) \cap (A \times A) \subseteq u \cap (A \times A)$
114	111 113	eqsstrd	$⊢ ({I ↾}_{X} \subseteq u \land A \subseteq X) \to {I ↾}_{A} \subseteq u \cap (A \times A)$
115	90 91 114	syl2anc	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to {I ↾}_{A} \subseteq u \cap (A \times A)$
116		simpr	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to v = u \cap (A \times A)$
117	115 116	sseqtrrd	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to {I ↾}_{A} \subseteq v$
118	117 55	r19.29a	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to {I ↾}_{A} \subseteq v$
119	14	ad3antrrr	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to A \times A \in V$
120		ustinvel	$⊢ (U \in UnifOn (X) \land u \in U) \to u^{-1} \in U$
121	87 88 120	syl2anc	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to u^{-1} \in U$
122	116	cnveqd	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to v^{-1} = {(u \cap (A \times A))}^{-1}$
123		cnvin	$⊢ {(u \cap (A \times A))}^{-1} = u^{-1} \cap {(A \times A)}^{-1}$
124		cnvxp	$⊢ {(A \times A)}^{-1} = A \times A$
125	124	ineq2i	$⊢ u^{-1} \cap {(A \times A)}^{-1} = u^{-1} \cap (A \times A)$
126	123 125	eqtri	$⊢ {(u \cap (A \times A))}^{-1} = u^{-1} \cap (A \times A)$
127	122 126	eqtrdi	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to v^{-1} = u^{-1} \cap (A \times A)$
128		ineq1	$⊢ x = u^{-1} \to x \cap (A \times A) = u^{-1} \cap (A \times A)$
129	128	rspceeqv	$⊢ (u^{-1} \in U \land v^{-1} = u^{-1} \cap (A \times A)) \to \exists x \in U v^{-1} = x \cap (A \times A)$
130	121 127 129	syl2anc	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to \exists x \in U v^{-1} = x \cap (A \times A)$
131		elrest	$⊢ (U \in UnifOn (X) \land A \times A \in V) \to (v^{-1} \in (U ↾_{𝑡} (A \times A)) \leftrightarrow \exists x \in U v^{-1} = x \cap (A \times A))$
132	131	biimpar	$⊢ ((U \in UnifOn (X) \land A \times A \in V) \land \exists x \in U v^{-1} = x \cap (A \times A)) \to v^{-1} \in (U ↾_{𝑡} (A \times A))$
133	87 119 130 132	syl21anc	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to v^{-1} \in (U ↾_{𝑡} (A \times A))$
134	133 55	r19.29a	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to v^{-1} \in (U ↾_{𝑡} (A \times A))$
135		simp-4l	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to U \in UnifOn (X)$
136	14	ad3antrrr	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to A \times A \in V$
137		simplr	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to x \in U$
138		elrestr	$⊢ (U \in UnifOn (X) \land A \times A \in V \land x \in U) \to x \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
139	135 136 137 138	syl3anc	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to x \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
140		inss1	$⊢ x \cap (A \times A) \subseteq x$
141		coss1	$⊢ x \cap (A \times A) \subseteq x \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq x \circ (x \cap (A \times A))$
142		coss2	$⊢ x \cap (A \times A) \subseteq x \to x \circ (x \cap (A \times A)) \subseteq x \circ x$
143	141 142	sstrd	$⊢ x \cap (A \times A) \subseteq x \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq x \circ x$
144	140 143	ax-mp	$⊢ (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq x \circ x$
145		sstr	$⊢ ((x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq x \circ x \land x \circ x \subseteq u) \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq u$
146	144 145	mpan	$⊢ x \circ x \subseteq u \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq u$
147	146	adantl	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq u$
148		inss2	$⊢ x \cap (A \times A) \subseteq A \times A$
149		coss1	$⊢ x \cap (A \times A) \subseteq A \times A \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq (A \times A) \circ (x \cap (A \times A))$
150		coss2	$⊢ x \cap (A \times A) \subseteq A \times A \to (A \times A) \circ (x \cap (A \times A)) \subseteq (A \times A) \circ (A \times A)$
151	149 150	sstrd	$⊢ x \cap (A \times A) \subseteq A \times A \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq (A \times A) \circ (A \times A)$
152	148 151	ax-mp	$⊢ (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq (A \times A) \circ (A \times A)$
153		xpidtr	$⊢ (A \times A) \circ (A \times A) \subseteq A \times A$
154	152 153	sstri	$⊢ (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq A \times A$
155	154	a1i	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq A \times A$
156	147 155	ssind	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq u \cap (A \times A)$
157		id	$⊢ w = x \cap (A \times A) \to w = x \cap (A \times A)$
158	157 157	coeq12d	$⊢ w = x \cap (A \times A) \to w \circ w = (x \cap (A \times A)) \circ (x \cap (A \times A))$
159	158	sseq1d	$⊢ w = x \cap (A \times A) \to (w \circ w \subseteq u \cap (A \times A) \leftrightarrow (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq u \cap (A \times A))$
160	159	rspcev	$⊢ (x \cap (A \times A) \in (U ↾_{𝑡} (A \times A)) \land (x \cap (A \times A)) \circ (x \cap (A \times A)) \subseteq u \cap (A \times A)) \to \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq u \cap (A \times A)$
161	139 156 160	syl2anc	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \land x \in U) \land x \circ x \subseteq u) \to \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq u \cap (A \times A)$
162		ustexhalf	$⊢ (U \in UnifOn (X) \land u \in U) \to \exists x \in U x \circ x \subseteq u$
163	162	adantlr	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \to \exists x \in U x \circ x \subseteq u$
164	161 163	r19.29a	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land u \in U) \to \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq u \cap (A \times A)$
165	164	ad4ant13	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq u \cap (A \times A)$
166	116	sseq2d	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to (w \circ w \subseteq v \leftrightarrow w \circ w \subseteq u \cap (A \times A))$
167	166	rexbidv	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to (\exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v \leftrightarrow \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq u \cap (A \times A))$
168	165 167	mpbird	$⊢ ((((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \land u \in U) \land v = u \cap (A \times A)) \to \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v$
169	168 55	r19.29a	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v$
170	118 134 169	3jca	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to ({I ↾}_{A} \subseteq v \land v^{-1} \in (U ↾_{𝑡} (A \times A)) \land \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v)$
171	59 86 170	3jca	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land v \in (U ↾_{𝑡} (A \times A))) \to (\forall w \in 𝒫 (A \times A) (v \subseteq w \to w \in (U ↾_{𝑡} (A \times A))) \land \forall w \in (U ↾_{𝑡} (A \times A)) v \cap w \in (U ↾_{𝑡} (A \times A)) \land ({I ↾}_{A} \subseteq v \land v^{-1} \in (U ↾_{𝑡} (A \times A)) \land \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v))$
172	171	ralrimiva	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to \forall v \in (U ↾_{𝑡} (A \times A)) (\forall w \in 𝒫 (A \times A) (v \subseteq w \to w \in (U ↾_{𝑡} (A \times A))) \land \forall w \in (U ↾_{𝑡} (A \times A)) v \cap w \in (U ↾_{𝑡} (A \times A)) \land ({I ↾}_{A} \subseteq v \land v^{-1} \in (U ↾_{𝑡} (A \times A)) \land \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v))$
173	2 19 172	3jca	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to (U ↾_{𝑡} (A \times A) \subseteq 𝒫 (A \times A) \land A \times A \in (U ↾_{𝑡} (A \times A)) \land \forall v \in (U ↾_{𝑡} (A \times A)) (\forall w \in 𝒫 (A \times A) (v \subseteq w \to w \in (U ↾_{𝑡} (A \times A))) \land \forall w \in (U ↾_{𝑡} (A \times A)) v \cap w \in (U ↾_{𝑡} (A \times A)) \land ({I ↾}_{A} \subseteq v \land v^{-1} \in (U ↾_{𝑡} (A \times A)) \land \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v)))$
174		isust	$⊢ A \in V \to (U ↾_{𝑡} (A \times A) \in UnifOn (A) \leftrightarrow (U ↾_{𝑡} (A \times A) \subseteq 𝒫 (A \times A) \land A \times A \in (U ↾_{𝑡} (A \times A)) \land \forall v \in (U ↾_{𝑡} (A \times A)) (\forall w \in 𝒫 (A \times A) (v \subseteq w \to w \in (U ↾_{𝑡} (A \times A))) \land \forall w \in (U ↾_{𝑡} (A \times A)) v \cap w \in (U ↾_{𝑡} (A \times A)) \land ({I ↾}_{A} \subseteq v \land v^{-1} \in (U ↾_{𝑡} (A \times A)) \land \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v))))$
175	13 174	syl	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to (U ↾_{𝑡} (A \times A) \in UnifOn (A) \leftrightarrow (U ↾_{𝑡} (A \times A) \subseteq 𝒫 (A \times A) \land A \times A \in (U ↾_{𝑡} (A \times A)) \land \forall v \in (U ↾_{𝑡} (A \times A)) (\forall w \in 𝒫 (A \times A) (v \subseteq w \to w \in (U ↾_{𝑡} (A \times A))) \land \forall w \in (U ↾_{𝑡} (A \times A)) v \cap w \in (U ↾_{𝑡} (A \times A)) \land ({I ↾}_{A} \subseteq v \land v^{-1} \in (U ↾_{𝑡} (A \times A)) \land \exists w \in (U ↾_{𝑡} (A \times A)) w \circ w \subseteq v))))$
176	173 175	mpbird	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$

Metamath Proof Explorer

Theorem trust

Proof