Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  restutopopn Structured version   Visualization version   GIF version

Theorem restutopopn 21961
 Description: The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017.)
Assertion
Ref Expression
restutopopn ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) = (unifTop‘(𝑈t (𝐴 × 𝐴))))

Proof of Theorem restutopopn
Dummy variables 𝑎 𝑏 𝑡 𝑢 𝑤 𝑥 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elutop 21956 . . . 4 (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴𝑋 ∧ ∀𝑥𝐴𝑡𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴)))
21simprbda 652 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → 𝐴𝑋)
3 restutop 21960 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈t (𝐴 × 𝐴))))
42, 3syldan 487 . 2 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈t (𝐴 × 𝐴))))
5 trust 21952 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝑈t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
62, 5syldan 487 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑈t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
7 elutop 21956 . . . . . . . . . 10 ((𝑈t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) → (𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴))) ↔ (𝑏𝐴 ∧ ∀𝑥𝑏𝑢 ∈ (𝑈t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏)))
86, 7syl 17 . . . . . . . . 9 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴))) ↔ (𝑏𝐴 ∧ ∀𝑥𝑏𝑢 ∈ (𝑈t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏)))
98simprbda 652 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → 𝑏𝐴)
102adantr 481 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → 𝐴𝑋)
119, 10sstrd 3597 . . . . . . 7 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → 𝑏𝑋)
12 simp-9l 815 . . . . . . . . . . . . 13 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑈 ∈ (UnifOn‘𝑋))
13 simplr 791 . . . . . . . . . . . . 13 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑡𝑈)
14 simp-4r 806 . . . . . . . . . . . . 13 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑤𝑈)
15 ustincl 21930 . . . . . . . . . . . . 13 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑡𝑈𝑤𝑈) → (𝑡𝑤) ∈ 𝑈)
1612, 13, 14, 15syl3anc 1323 . . . . . . . . . . . 12 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑡𝑤) ∈ 𝑈)
17 inimass 5513 . . . . . . . . . . . . 13 ((𝑡𝑤) “ {𝑥}) ⊆ ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥}))
18 ssrin 3821 . . . . . . . . . . . . . . . 16 ((𝑡 “ {𝑥}) ⊆ 𝐴 → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝐴 ∩ (𝑤 “ {𝑥})))
1918adantl 482 . . . . . . . . . . . . . . 15 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝐴 ∩ (𝑤 “ {𝑥})))
20 simpllr 798 . . . . . . . . . . . . . . . . 17 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑢 = (𝑤 ∩ (𝐴 × 𝐴)))
2120imaeq1d 5429 . . . . . . . . . . . . . . . 16 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) = ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}))
229ad5antr 769 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑏𝐴)
23 simp-5r 808 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑥𝑏)
2422, 23sseldd 3588 . . . . . . . . . . . . . . . . . 18 ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑥𝐴)
2524ad2antrr 761 . . . . . . . . . . . . . . . . 17 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑥𝐴)
26 vex 3192 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
27 inimasn 5514 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ V → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥})))
2826, 27ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥}))
29 xpimasn 5543 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴 → ((𝐴 × 𝐴) “ {𝑥}) = 𝐴)
3029ineq2d 3797 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 → ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥})) = ((𝑤 “ {𝑥}) ∩ 𝐴))
3128, 30syl5eq 2667 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ 𝐴))
32 incom 3788 . . . . . . . . . . . . . . . . . 18 ((𝑤 “ {𝑥}) ∩ 𝐴) = (𝐴 ∩ (𝑤 “ {𝑥}))
3331, 32syl6eq 2671 . . . . . . . . . . . . . . . . 17 (𝑥𝐴 → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥})))
3425, 33syl 17 . . . . . . . . . . . . . . . 16 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥})))
3521, 34eqtrd 2655 . . . . . . . . . . . . . . 15 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥})))
3619, 35sseqtr4d 3626 . . . . . . . . . . . . . 14 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝑢 “ {𝑥}))
37 simp-5r 808 . . . . . . . . . . . . . 14 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) ⊆ 𝑏)
3836, 37sstrd 3597 . . . . . . . . . . . . 13 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ 𝑏)
3917, 38syl5ss 3598 . . . . . . . . . . . 12 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡𝑤) “ {𝑥}) ⊆ 𝑏)
40 imaeq1 5425 . . . . . . . . . . . . . 14 (𝑣 = (𝑡𝑤) → (𝑣 “ {𝑥}) = ((𝑡𝑤) “ {𝑥}))
4140sseq1d 3616 . . . . . . . . . . . . 13 (𝑣 = (𝑡𝑤) → ((𝑣 “ {𝑥}) ⊆ 𝑏 ↔ ((𝑡𝑤) “ {𝑥}) ⊆ 𝑏))
4241rspcev 3298 . . . . . . . . . . . 12 (((𝑡𝑤) ∈ 𝑈 ∧ ((𝑡𝑤) “ {𝑥}) ⊆ 𝑏) → ∃𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)
4316, 39, 42syl2anc 692 . . . . . . . . . . 11 ((((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ∃𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)
44 simp-4l 805 . . . . . . . . . . . . 13 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)))
4544ad2antrr 761 . . . . . . . . . . . 12 ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)))
461simplbda 653 . . . . . . . . . . . . 13 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ∀𝑥𝐴𝑡𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴)
4746r19.21bi 2927 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑥𝐴) → ∃𝑡𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴)
4845, 24, 47syl2anc 692 . . . . . . . . . . 11 ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → ∃𝑡𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴)
4943, 48r19.29a 3072 . . . . . . . . . 10 ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → ∃𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)
50 simplr 791 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → 𝑢 ∈ (𝑈t (𝐴 × 𝐴)))
51 sqxpexg 6923 . . . . . . . . . . . . 13 (𝐴 ∈ (unifTop‘𝑈) → (𝐴 × 𝐴) ∈ V)
52 elrest 16016 . . . . . . . . . . . . 13 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑢 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑤𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))))
5351, 52sylan2 491 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑢 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑤𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))))
5453biimpa 501 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑤𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴)))
5544, 50, 54syl2anc 692 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → ∃𝑤𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴)))
5649, 55r19.29a 3072 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) ∧ 𝑢 ∈ (𝑈t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → ∃𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)
578simplbda 653 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → ∀𝑥𝑏𝑢 ∈ (𝑈t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏)
5857r19.21bi 2927 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) → ∃𝑢 ∈ (𝑈t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏)
5956, 58r19.29a 3072 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) ∧ 𝑥𝑏) → ∃𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)
6059ralrimiva 2961 . . . . . . 7 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → ∀𝑥𝑏𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)
61 elutop 21956 . . . . . . . 8 (𝑈 ∈ (UnifOn‘𝑋) → (𝑏 ∈ (unifTop‘𝑈) ↔ (𝑏𝑋 ∧ ∀𝑥𝑏𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)))
6261ad2antrr 761 . . . . . . 7 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → (𝑏 ∈ (unifTop‘𝑈) ↔ (𝑏𝑋 ∧ ∀𝑥𝑏𝑣𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏)))
6311, 60, 62mpbir2and 956 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → 𝑏 ∈ (unifTop‘𝑈))
64 df-ss 3573 . . . . . . . 8 (𝑏𝐴 ↔ (𝑏𝐴) = 𝑏)
659, 64sylib 208 . . . . . . 7 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → (𝑏𝐴) = 𝑏)
6665eqcomd 2627 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → 𝑏 = (𝑏𝐴))
67 ineq1 3790 . . . . . . . 8 (𝑎 = 𝑏 → (𝑎𝐴) = (𝑏𝐴))
6867eqeq2d 2631 . . . . . . 7 (𝑎 = 𝑏 → (𝑏 = (𝑎𝐴) ↔ 𝑏 = (𝑏𝐴)))
6968rspcev 3298 . . . . . 6 ((𝑏 ∈ (unifTop‘𝑈) ∧ 𝑏 = (𝑏𝐴)) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎𝐴))
7063, 66, 69syl2anc 692 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎𝐴))
71 fvex 6163 . . . . . . 7 (unifTop‘𝑈) ∈ V
72 elrest 16016 . . . . . . 7 (((unifTop‘𝑈) ∈ V ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎𝐴)))
7371, 72mpan 705 . . . . . 6 (𝐴 ∈ (unifTop‘𝑈) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎𝐴)))
7473ad2antlr 762 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎𝐴)))
7570, 74mpbird 247 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴)))) → 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴))
7675ex 450 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑏 ∈ (unifTop‘(𝑈t (𝐴 × 𝐴))) → 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)))
7776ssrdv 3593 . 2 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (unifTop‘(𝑈t (𝐴 × 𝐴))) ⊆ ((unifTop‘𝑈) ↾t 𝐴))
784, 77eqssd 3604 1 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) = (unifTop‘(𝑈t (𝐴 × 𝐴))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  Vcvv 3189   ∩ cin 3558   ⊆ wss 3559  {csn 4153   × cxp 5077   “ cima 5082  ‘cfv 5852  (class class class)co 6610   ↾t crest 16009  UnifOncust 21922  unifTopcutop 21953 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-1st 7120  df-2nd 7121  df-rest 16011  df-ust 21923  df-utop 21954 This theorem is referenced by:  ressusp  21988
 Copyright terms: Public domain W3C validator