Step | Hyp | Ref
| Expression |
1 | | elutop 22037 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴))) |
2 | 1 | simprbda 653 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → 𝐴 ⊆ 𝑋) |
3 | | restutop 22041 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |
4 | 2, 3 | syldan 487 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |
5 | | trust 22033 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴)) |
6 | 2, 5 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴)) |
7 | | elutop 22037 |
. . . . . . . . . 10
⊢ ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏))) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏))) |
9 | 8 | simprbda 653 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ⊆ 𝐴) |
10 | 2 | adantr 481 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝐴 ⊆ 𝑋) |
11 | 9, 10 | sstrd 3613 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ⊆ 𝑋) |
12 | | simp-9l 816 |
. . . . . . . . . . . . 13
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑈 ∈ (UnifOn‘𝑋)) |
13 | | simplr 792 |
. . . . . . . . . . . . 13
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑡 ∈ 𝑈) |
14 | | simp-4r 807 |
. . . . . . . . . . . . 13
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑤 ∈ 𝑈) |
15 | | ustincl 22011 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑡 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈) → (𝑡 ∩ 𝑤) ∈ 𝑈) |
16 | 12, 13, 14, 15 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑡 ∩ 𝑤) ∈ 𝑈) |
17 | | inimass 5549 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) |
18 | | ssrin 3838 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 “ {𝑥}) ⊆ 𝐴 → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝐴 ∩ (𝑤 “ {𝑥}))) |
19 | 18 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝐴 ∩ (𝑤 “ {𝑥}))) |
20 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) |
21 | 20 | imaeq1d 5465 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) = ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥})) |
22 | 9 | ad5antr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑏 ⊆ 𝐴) |
23 | | simp-5r 809 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑥 ∈ 𝑏) |
24 | 22, 23 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑥 ∈ 𝐴) |
25 | 24 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑥 ∈ 𝐴) |
26 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
27 | | inimasn 5550 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ V → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥}))) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥})) |
29 | | xpimasn 5579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 → ((𝐴 × 𝐴) “ {𝑥}) = 𝐴) |
30 | 29 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥})) = ((𝑤 “ {𝑥}) ∩ 𝐴)) |
31 | 28, 30 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐴 → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ 𝐴)) |
32 | | incom 3805 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 “ {𝑥}) ∩ 𝐴) = (𝐴 ∩ (𝑤 “ {𝑥})) |
33 | 31, 32 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥}))) |
34 | 25, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥}))) |
35 | 21, 34 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥}))) |
36 | 19, 35 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝑢 “ {𝑥})) |
37 | | simp-5r 809 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) ⊆ 𝑏) |
38 | 36, 37 | sstrd 3613 |
. . . . . . . . . . . . 13
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ 𝑏) |
39 | 17, 38 | syl5ss 3614 |
. . . . . . . . . . . 12
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ 𝑏) |
40 | | imaeq1 5461 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑡 ∩ 𝑤) → (𝑣 “ {𝑥}) = ((𝑡 ∩ 𝑤) “ {𝑥})) |
41 | 40 | sseq1d 3632 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑡 ∩ 𝑤) → ((𝑣 “ {𝑥}) ⊆ 𝑏 ↔ ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ 𝑏)) |
42 | 41 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∩ 𝑤) ∈ 𝑈 ∧ ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ 𝑏) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
43 | 16, 39, 42 | syl2anc 693 |
. . . . . . . . . . 11
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
44 | | simp-4l 806 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈))) |
45 | 44 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈))) |
46 | 1 | simplbda 654 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ∀𝑥 ∈ 𝐴 ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴) |
47 | 46 | r19.21bi 2932 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑥 ∈ 𝐴) → ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴) |
48 | 45, 24, 47 | syl2anc 693 |
. . . . . . . . . . 11
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴) |
49 | 43, 48 | r19.29a 3078 |
. . . . . . . . . 10
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
50 | | simplr 792 |
. . . . . . . . . . 11
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) |
51 | | sqxpexg 6963 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (unifTop‘𝑈) → (𝐴 × 𝐴) ∈ V) |
52 | | elrest 16088 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴)))) |
53 | 51, 52 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴)))) |
54 | 53 | biimpa 501 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) |
55 | 44, 50, 54 | syl2anc 693 |
. . . . . . . . . 10
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) |
56 | 49, 55 | r19.29a 3078 |
. . . . . . . . 9
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
57 | 8 | simplbda 654 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → ∀𝑥 ∈ 𝑏 ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏) |
58 | 57 | r19.21bi 2932 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) ∧ 𝑥 ∈ 𝑏) → ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏) |
59 | 56, 58 | r19.29a 3078 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) ∧ 𝑥 ∈ 𝑏) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
60 | 59 | ralrimiva 2966 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
61 | | elutop 22037 |
. . . . . . . 8
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑏 ∈ (unifTop‘𝑈) ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏))) |
62 | 61 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → (𝑏 ∈ (unifTop‘𝑈) ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏))) |
63 | 11, 60, 62 | mpbir2and 957 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ∈ (unifTop‘𝑈)) |
64 | | df-ss 3588 |
. . . . . . . 8
⊢ (𝑏 ⊆ 𝐴 ↔ (𝑏 ∩ 𝐴) = 𝑏) |
65 | 9, 64 | sylib 208 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → (𝑏 ∩ 𝐴) = 𝑏) |
66 | 65 | eqcomd 2628 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 = (𝑏 ∩ 𝐴)) |
67 | | ineq1 3807 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑎 ∩ 𝐴) = (𝑏 ∩ 𝐴)) |
68 | 67 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑏 = (𝑎 ∩ 𝐴) ↔ 𝑏 = (𝑏 ∩ 𝐴))) |
69 | 68 | rspcev 3309 |
. . . . . 6
⊢ ((𝑏 ∈ (unifTop‘𝑈) ∧ 𝑏 = (𝑏 ∩ 𝐴)) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)) |
70 | 63, 66, 69 | syl2anc 693 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)) |
71 | | fvex 6201 |
. . . . . . 7
⊢
(unifTop‘𝑈)
∈ V |
72 | | elrest 16088 |
. . . . . . 7
⊢
(((unifTop‘𝑈)
∈ V ∧ 𝐴 ∈
(unifTop‘𝑈)) →
(𝑏 ∈
((unifTop‘𝑈)
↾t 𝐴)
↔ ∃𝑎 ∈
(unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
73 | 71, 72 | mpan 706 |
. . . . . 6
⊢ (𝐴 ∈ (unifTop‘𝑈) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
74 | 73 | ad2antlr 763 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
75 | 70, 74 | mpbird 247 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) |
76 | 75 | ex 450 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) → 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴))) |
77 | 76 | ssrdv 3609 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ⊆ ((unifTop‘𝑈) ↾t 𝐴)) |
78 | 4, 77 | eqssd 3620 |
1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) = (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |