Metamath Proof Explorer

Theorem restutopopn

Description: The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑡 ∈ 𝑈 ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) ) )
2 1 simprbda ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → 𝐴 ⊆ 𝑋 )
3 restutop ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ⊆ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )
4 2 3 syldan ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ⊆ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )
5 trust ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
6 2 5 syldan ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
7 elutop ⊢ ( ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) → ( 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑏 ∃ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ) )
8 6 7 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑏 ∃ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ) )
9 8 simprbda ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝑏 ⊆ 𝐴 )
10 2 adantr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐴 ⊆ 𝑋 )
11 9 10 sstrd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝑏 ⊆ 𝑋 )
12 simp-9l ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
13 simplr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → 𝑡 ∈ 𝑈 )
14 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → 𝑤 ∈ 𝑈 )
15 ustincl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈 ) → ( 𝑡 ∩ 𝑤 ) ∈ 𝑈 )
16 12 13 14 15 syl3anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( 𝑡 ∩ 𝑤 ) ∈ 𝑈 )
17 inimass ⊢ ( ( 𝑡 ∩ 𝑤 ) “ { 𝑥 } ) ⊆ ( ( 𝑡 “ { 𝑥 } ) ∩ ( 𝑤 “ { 𝑥 } ) )
18 ssrin ⊢ ( ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 → ( ( 𝑡 “ { 𝑥 } ) ∩ ( 𝑤 “ { 𝑥 } ) ) ⊆ ( 𝐴 ∩ ( 𝑤 “ { 𝑥 } ) ) )
19 18 adantl ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( ( 𝑡 “ { 𝑥 } ) ∩ ( 𝑤 “ { 𝑥 } ) ) ⊆ ( 𝐴 ∩ ( 𝑤 “ { 𝑥 } ) ) )
20 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) )
21 20 imaeq1d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( 𝑢 “ { 𝑥 } ) = ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) )
22 9 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) → 𝑏 ⊆ 𝐴 )
23 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) → 𝑥 ∈ 𝑏 )
24 22 23 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) → 𝑥 ∈ 𝐴 )
25 24 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → 𝑥 ∈ 𝐴 )
26 inimasn ⊢ ( 𝑥 ∈ V → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) = ( ( 𝑤 “ { 𝑥 } ) ∩ ( ( 𝐴 × 𝐴 ) “ { 𝑥 } ) ) )
27 26 elv ⊢ ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) = ( ( 𝑤 “ { 𝑥 } ) ∩ ( ( 𝐴 × 𝐴 ) “ { 𝑥 } ) )
28 xpimasn ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 × 𝐴 ) “ { 𝑥 } ) = 𝐴 )
29 28 ineq2d ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑤 “ { 𝑥 } ) ∩ ( ( 𝐴 × 𝐴 ) “ { 𝑥 } ) ) = ( ( 𝑤 “ { 𝑥 } ) ∩ 𝐴 ) )
30 27 29 syl5eq ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) = ( ( 𝑤 “ { 𝑥 } ) ∩ 𝐴 ) )
31 incom ⊢ ( ( 𝑤 “ { 𝑥 } ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝑤 “ { 𝑥 } ) )
32 30 31 eqtrdi ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) = ( 𝐴 ∩ ( 𝑤 “ { 𝑥 } ) ) )
33 25 32 syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝑥 } ) = ( 𝐴 ∩ ( 𝑤 “ { 𝑥 } ) ) )
34 21 33 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( 𝑢 “ { 𝑥 } ) = ( 𝐴 ∩ ( 𝑤 “ { 𝑥 } ) ) )
35 19 34 sseqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( ( 𝑡 “ { 𝑥 } ) ∩ ( 𝑤 “ { 𝑥 } ) ) ⊆ ( 𝑢 “ { 𝑥 } ) )
36 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 )
37 35 36 sstrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( ( 𝑡 “ { 𝑥 } ) ∩ ( 𝑤 “ { 𝑥 } ) ) ⊆ 𝑏 )
38 17 37 sstrid ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ( ( 𝑡 ∩ 𝑤 ) “ { 𝑥 } ) ⊆ 𝑏 )
39 imaeq1 ⊢ ( 𝑣 = ( 𝑡 ∩ 𝑤 ) → ( 𝑣 “ { 𝑥 } ) = ( ( 𝑡 ∩ 𝑤 ) “ { 𝑥 } ) )
40 39 sseq1d ⊢ ( 𝑣 = ( 𝑡 ∩ 𝑤 ) → ( ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 ↔ ( ( 𝑡 ∩ 𝑤 ) “ { 𝑥 } ) ⊆ 𝑏 ) )
41 40 rspcev ⊢ ( ( ( 𝑡 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( 𝑡 ∩ 𝑤 ) “ { 𝑥 } ) ⊆ 𝑏 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
42 16 38 41 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑡 ∈ 𝑈 ) ∧ ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
43 simp-4l ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) )
44 43 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) )
45 1 simplbda ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑡 ∈ 𝑈 ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 )
46 45 r19.21bi ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑡 ∈ 𝑈 ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 )
47 44 24 46 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑡 ∈ 𝑈 ( 𝑡 “ { 𝑥 } ) ⊆ 𝐴 )
48 42 47 r19.29a ⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
49 simplr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) → 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) )
50 sqxpexg ⊢ ( 𝐴 ∈ ( unifTop ‘ 𝑈 ) → ( 𝐴 × 𝐴 ) ∈ V )
51 elrest ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐴 × 𝐴 ) ∈ V ) → ( 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ↔ ∃ 𝑤 ∈ 𝑈 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) )
52 50 51 sylan2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ↔ ∃ 𝑤 ∈ 𝑈 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ) )
53 52 biimpa ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑤 ∈ 𝑈 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) )
54 43 49 53 syl2anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) → ∃ 𝑤 ∈ 𝑈 𝑢 = ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) )
55 48 54 r19.29a ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) ∧ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
56 8 simplbda ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ∀ 𝑥 ∈ 𝑏 ∃ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 )
57 56 r19.21bi ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) → ∃ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ( 𝑢 “ { 𝑥 } ) ⊆ 𝑏 )
58 55 57 r19.29a ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑥 ∈ 𝑏 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
59 58 ralrimiva ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ∀ 𝑥 ∈ 𝑏 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 )
60 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑏 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑏 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 ) ) )
61 60 ad2antrr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ( 𝑏 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑏 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑏 ) ) )
62 11 59 61 mpbir2and ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝑏 ∈ ( unifTop ‘ 𝑈 ) )
63 df-ss ⊢ ( 𝑏 ⊆ 𝐴 ↔ ( 𝑏 ∩ 𝐴 ) = 𝑏 )
64 9 63 sylib ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ( 𝑏 ∩ 𝐴 ) = 𝑏 )
65 64 eqcomd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝑏 = ( 𝑏 ∩ 𝐴 ) )
66 ineq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ∩ 𝐴 ) = ( 𝑏 ∩ 𝐴 ) )
67 66 rspceeqv ⊢ ( ( 𝑏 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑏 = ( 𝑏 ∩ 𝐴 ) ) → ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) )
68 62 65 67 syl2anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) )
69 fvex ⊢ ( unifTop ‘ 𝑈 ) ∈ V
70 elrest ⊢ ( ( ( unifTop ‘ 𝑈 ) ∈ V ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) ) )
71 69 70 mpan ⊢ ( 𝐴 ∈ ( unifTop ‘ 𝑈 ) → ( 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) ) )
72 71 ad2antlr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ( 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ ( unifTop ‘ 𝑈 ) 𝑏 = ( 𝑎 ∩ 𝐴 ) ) )
73 68 72 mpbird ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑏 ∈ ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝑏 ∈ ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) )
74 4 73 eqelssd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ∈ ( unifTop ‘ 𝑈 ) ) → ( ( unifTop ‘ 𝑈 ) ↾t 𝐴 ) = ( unifTop ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )