Step | Hyp | Ref
| Expression |
1 | | elutop 23375 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴))) |
2 | 1 | simprbda 499 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → 𝐴 ⊆ 𝑋) |
3 | | restutop 23379 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |
4 | 2, 3 | syldan 591 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |
5 | | trust 23371 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴)) |
6 | 2, 5 | syldan 591 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴)) |
7 | | elutop 23375 |
. . . . . . . 8
⊢ ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏))) |
9 | 8 | simprbda 499 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ⊆ 𝐴) |
10 | 2 | adantr 481 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝐴 ⊆ 𝑋) |
11 | 9, 10 | sstrd 3936 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ⊆ 𝑋) |
12 | | simp-9l 790 |
. . . . . . . . . . 11
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑈 ∈ (UnifOn‘𝑋)) |
13 | | simplr 766 |
. . . . . . . . . . 11
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑡 ∈ 𝑈) |
14 | | simp-4r 781 |
. . . . . . . . . . 11
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑤 ∈ 𝑈) |
15 | | ustincl 23349 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑡 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈) → (𝑡 ∩ 𝑤) ∈ 𝑈) |
16 | 12, 13, 14, 15 | syl3anc 1370 |
. . . . . . . . . 10
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑡 ∩ 𝑤) ∈ 𝑈) |
17 | | inimass 6056 |
. . . . . . . . . . 11
⊢ ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) |
18 | | ssrin 4173 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 “ {𝑥}) ⊆ 𝐴 → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝐴 ∩ (𝑤 “ {𝑥}))) |
19 | 18 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝐴 ∩ (𝑤 “ {𝑥}))) |
20 | | simpllr 773 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) |
21 | 20 | imaeq1d 5966 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) = ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥})) |
22 | 9 | ad5antr 731 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑏 ⊆ 𝐴) |
23 | | simp-5r 783 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑥 ∈ 𝑏) |
24 | 22, 23 | sseldd 3927 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → 𝑥 ∈ 𝐴) |
25 | 24 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → 𝑥 ∈ 𝐴) |
26 | | inimasn 6057 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ V → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥}))) |
27 | 26 | elv 3437 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥})) |
28 | | xpimasn 6086 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐴 → ((𝐴 × 𝐴) “ {𝑥}) = 𝐴) |
29 | 28 | ineq2d 4152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝑤 “ {𝑥}) ∩ ((𝐴 × 𝐴) “ {𝑥})) = ((𝑤 “ {𝑥}) ∩ 𝐴)) |
30 | 27, 29 | eqtrid 2792 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = ((𝑤 “ {𝑥}) ∩ 𝐴)) |
31 | | incom 4140 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 “ {𝑥}) ∩ 𝐴) = (𝐴 ∩ (𝑤 “ {𝑥})) |
32 | 30, 31 | eqtrdi 2796 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥}))) |
33 | 25, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑤 ∩ (𝐴 × 𝐴)) “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥}))) |
34 | 21, 33 | eqtrd 2780 |
. . . . . . . . . . . . 13
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) = (𝐴 ∩ (𝑤 “ {𝑥}))) |
35 | 19, 34 | sseqtrrd 3967 |
. . . . . . . . . . . 12
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ (𝑢 “ {𝑥})) |
36 | | simp-5r 783 |
. . . . . . . . . . . 12
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → (𝑢 “ {𝑥}) ⊆ 𝑏) |
37 | 35, 36 | sstrd 3936 |
. . . . . . . . . . 11
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 “ {𝑥}) ∩ (𝑤 “ {𝑥})) ⊆ 𝑏) |
38 | 17, 37 | sstrid 3937 |
. . . . . . . . . 10
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ 𝑏) |
39 | | imaeq1 5962 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑡 ∩ 𝑤) → (𝑣 “ {𝑥}) = ((𝑡 ∩ 𝑤) “ {𝑥})) |
40 | 39 | sseq1d 3957 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑡 ∩ 𝑤) → ((𝑣 “ {𝑥}) ⊆ 𝑏 ↔ ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ 𝑏)) |
41 | 40 | rspcev 3561 |
. . . . . . . . . 10
⊢ (((𝑡 ∩ 𝑤) ∈ 𝑈 ∧ ((𝑡 ∩ 𝑤) “ {𝑥}) ⊆ 𝑏) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
42 | 16, 38, 41 | syl2anc 584 |
. . . . . . . . 9
⊢
((((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) ∧ 𝑡 ∈ 𝑈) ∧ (𝑡 “ {𝑥}) ⊆ 𝐴) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
43 | | simp-4l 780 |
. . . . . . . . . . 11
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈))) |
44 | 43 | ad2antrr 723 |
. . . . . . . . . 10
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈))) |
45 | 1 | simplbda 500 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ∀𝑥 ∈ 𝐴 ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴) |
46 | 45 | r19.21bi 3135 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑥 ∈ 𝐴) → ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴) |
47 | 44, 24, 46 | syl2anc 584 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → ∃𝑡 ∈ 𝑈 (𝑡 “ {𝑥}) ⊆ 𝐴) |
48 | 42, 47 | r19.29a 3220 |
. . . . . . . 8
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
49 | | simplr 766 |
. . . . . . . . 9
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) |
50 | | sqxpexg 7597 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (unifTop‘𝑈) → (𝐴 × 𝐴) ∈ V) |
51 | | elrest 17128 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴)))) |
52 | 50, 51 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → (𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴)) ↔ ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴)))) |
53 | 52 | biimpa 477 |
. . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) → ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) |
54 | 43, 49, 53 | syl2anc 584 |
. . . . . . . 8
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → ∃𝑤 ∈ 𝑈 𝑢 = (𝑤 ∩ (𝐴 × 𝐴))) |
55 | 48, 54 | r19.29a 3220 |
. . . . . . 7
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ∈
(unifTop‘𝑈)) ∧
𝑏 ∈
(unifTop‘(𝑈
↾t (𝐴
× 𝐴)))) ∧ 𝑥 ∈ 𝑏) ∧ 𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))) ∧ (𝑢 “ {𝑥}) ⊆ 𝑏) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
56 | 8 | simplbda 500 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → ∀𝑥 ∈ 𝑏 ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏) |
57 | 56 | r19.21bi 3135 |
. . . . . . 7
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) ∧ 𝑥 ∈ 𝑏) → ∃𝑢 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑢 “ {𝑥}) ⊆ 𝑏) |
58 | 55, 57 | r19.29a 3220 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) ∧ 𝑥 ∈ 𝑏) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
59 | 58 | ralrimiva 3110 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏) |
60 | | elutop 23375 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑏 ∈ (unifTop‘𝑈) ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏))) |
61 | 60 | ad2antrr 723 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → (𝑏 ∈ (unifTop‘𝑈) ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑏))) |
62 | 11, 59, 61 | mpbir2and 710 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ∈ (unifTop‘𝑈)) |
63 | | df-ss 3909 |
. . . . . 6
⊢ (𝑏 ⊆ 𝐴 ↔ (𝑏 ∩ 𝐴) = 𝑏) |
64 | 9, 63 | sylib 217 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → (𝑏 ∩ 𝐴) = 𝑏) |
65 | 64 | eqcomd 2746 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 = (𝑏 ∩ 𝐴)) |
66 | | ineq1 4145 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝑎 ∩ 𝐴) = (𝑏 ∩ 𝐴)) |
67 | 66 | rspceeqv 3576 |
. . . 4
⊢ ((𝑏 ∈ (unifTop‘𝑈) ∧ 𝑏 = (𝑏 ∩ 𝐴)) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)) |
68 | 62, 65, 67 | syl2anc 584 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)) |
69 | | fvex 6782 |
. . . . 5
⊢
(unifTop‘𝑈)
∈ V |
70 | | elrest 17128 |
. . . . 5
⊢
(((unifTop‘𝑈)
∈ V ∧ 𝐴 ∈
(unifTop‘𝑈)) →
(𝑏 ∈
((unifTop‘𝑈)
↾t 𝐴)
↔ ∃𝑎 ∈
(unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
71 | 69, 70 | mpan 687 |
. . . 4
⊢ (𝐴 ∈ (unifTop‘𝑈) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
72 | 71 | ad2antlr 724 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
73 | 68, 72 | mpbird 256 |
. 2
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) ∧ 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) |
74 | 4, 73 | eqelssd 3947 |
1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) = (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |