Metamath Proof Explorer

Theorem restutop

Description: Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017)

Ref Expression
Assertion restutop ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ⊆ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) )
2 fvexd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ V )
3 elfvex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
4 3 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ∈ V )
5 simpr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
6 4 5 ssexd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
7 elrest ⊢ ( ( ( unifTop ‘ 𝑈 ) ∈ V ∧ 𝐴 ∈ V ) → ( 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) ) )
8 2 6 7 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) ) )
9 8 biimpa ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) → ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) )
10 inss2 ⊢ ( 𝑎 ∩ 𝐴 ) ⊆ 𝐴
11 sseq1 ⊢ ( 𝑏 = ( 𝑎 ∩ 𝐴 ) → ( 𝑏 ⊆ 𝐴 ↔ ( 𝑎 ∩ 𝐴 ) ⊆ 𝐴 ) )
12 10 11 mpbiri ⊢ ( 𝑏 = ( 𝑎 ∩ 𝐴 ) → 𝑏 ⊆ 𝐴 )
13 12 rexlimivw ⊢ ( ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) → 𝑏 ⊆ 𝐴 )
14 9 13 syl ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) → 𝑏 ⊆ 𝐴 )
15 simp-5l ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
16 15 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
17 6 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝐴 ∈ V )
18 17 17 xpexd ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → ( 𝐴 × 𝐴 ) ∈ V )
19 simplr ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑢 ∈ 𝑈 )
20 elrestr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐴 × 𝐴 ) ∈ V ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) )
21 16 18 19 20 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) )
22 inss1 ⊢ ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑢
23 imass1 ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑢 → ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ( 𝑢 “ { 𝑥 } ) )
24 22 23 ax-mp ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ( 𝑢 “ { 𝑥 } )
25 sstr ⊢ ( ( ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ( 𝑢 “ { 𝑥 } ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ 𝑎 )
26 24 25 mpan ⊢ ( ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 → ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ 𝑎 )
27 imassrn ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ran ( 𝑢 ∩ ( 𝐴 × 𝐴 ) )
28 rnin ⊢ ran ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( ran 𝑢 ∩ ran ( 𝐴 × 𝐴 ) )
29 27 28 sstri ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ( ran 𝑢 ∩ ran ( 𝐴 × 𝐴 ) )
30 inss2 ⊢ ( ran 𝑢 ∩ ran ( 𝐴 × 𝐴 ) ) ⊆ ran ( 𝐴 × 𝐴 )
31 29 30 sstri ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ran ( 𝐴 × 𝐴 )
32 rnxpid ⊢ ran ( 𝐴 × 𝐴 ) = 𝐴
33 31 32 sseqtri ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ 𝐴
34 33 a1i ⊢ ( ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 → ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ 𝐴 )
35 26 34 ssind ⊢ ( ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 → ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ( 𝑎 ∩ 𝐴 ) )
36 35 adantl ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ ( 𝑎 ∩ 𝐴 ) )
37 simpllr ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑏 = ( 𝑎 ∩ 𝐴 ) )
38 36 37 sseqtrrd ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ 𝑏 )
39 imaeq1 ⊢ ( 𝑣 = ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑣 “ { 𝑥 } ) = ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) )
40 39 sseq1d ⊢ ( 𝑣 = ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 ↔ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ 𝑏 ) )
41 40 rspcev ⊢ ( ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) ⊆ 𝑏 ) → ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
42 21 38 41 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) → ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
43 simplr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → 𝑎 ∈ ( unifTop ‘ 𝑈 ) )
44 simpllr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → 𝑥 ∈ 𝑏 )
45 simpr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → 𝑏 = ( 𝑎 ∩ 𝐴 ) )
46 44 45 eleqtrd ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → 𝑥 ∈ ( 𝑎 ∩ 𝐴 ) )
47 46 elin1d ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → 𝑥 ∈ 𝑎 )
48 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑎 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑎 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 ) ) )
49 48 simplbda ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑥 ∈ 𝑎 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 )
50 49 r19.21bi ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 )
51 15 43 47 50 syl21anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑥 } ) ⊆ 𝑎 )
52 42 51 r19.29a ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑎 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 = ( 𝑎 ∩ 𝐴 ) ) → ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
53 9 adantr ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) → ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) )
54 52 53 r19.29a ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) ∧ 𝑥 ∈ 𝑏 ) → ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
55 54 ralrimiva ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) → ∀ 𝑥 ∈ 𝑏 ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
56 trust ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
57 elutop ⊢ ( ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) → ( 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑏 ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 ) ) )
58 56 57 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑏 ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 ) ) )
59 58 biimpar ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑏 ∃ 𝑣 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 ) ) → 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )
60 1 14 55 59 syl12anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ) → 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )
61 60 ex ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) → 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) )
62 61 ssrdv ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ⊆ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )