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 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )

Proof

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