# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {U}{↾}_{𝑡}\left({A}×{A}\right)\in \mathrm{UnifOn}\left({A}\right)$

### Proof

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