Step | Hyp | Ref
| Expression |
1 | | nfv 2015 |
. . . 4
⊢
Ⅎ𝑦((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) |
2 | | nfcv 2969 |
. . . 4
⊢
Ⅎ𝑦(𝑅 “ {𝐴}) |
3 | | nfrab1 3333 |
. . . 4
⊢
Ⅎ𝑦{𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} |
4 | | simprl 789 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾))) |
5 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐽
×t 𝐾) =
∪ (𝐽 ×t 𝐾) |
6 | 5 | cldss 21204 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) → 𝑅 ⊆ ∪ (𝐽 ×t 𝐾)) |
7 | 4, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ⊆ ∪ (𝐽 ×t 𝐾)) |
8 | | imasnopn.1 |
. . . . . . . . . . . . 13
⊢ 𝑋 = ∪
𝐽 |
9 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐾 =
∪ 𝐾 |
10 | 8, 9 | txuni 21766 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × ∪ 𝐾) =
∪ (𝐽 ×t 𝐾)) |
11 | 10 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑋 × ∪ 𝐾) = ∪
(𝐽 ×t
𝐾)) |
12 | 7, 11 | sseqtr4d 3867 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ⊆ (𝑋 × ∪ 𝐾)) |
13 | | imass1 5741 |
. . . . . . . . . 10
⊢ (𝑅 ⊆ (𝑋 × ∪ 𝐾) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × ∪ 𝐾) “ {𝐴})) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × ∪ 𝐾) “ {𝐴})) |
15 | | xpimasn 5820 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑋 → ((𝑋 × ∪ 𝐾) “ {𝐴}) = ∪ 𝐾) |
16 | 15 | ad2antll 722 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → ((𝑋 × ∪ 𝐾) “ {𝐴}) = ∪ 𝐾) |
17 | 14, 16 | sseqtrd 3866 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ⊆ ∪
𝐾) |
18 | 17 | sseld 3826 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) → 𝑦 ∈ ∪ 𝐾)) |
19 | 18 | pm4.71rd 560 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ (𝑅 “ {𝐴})))) |
20 | | elimasng 5732 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ V) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
21 | 20 | elvd 3419 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
22 | 21 | ad2antll 722 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
23 | 22 | anbi2d 624 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → ((𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ (𝑅 “ {𝐴})) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅))) |
24 | 19, 23 | bitrd 271 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅))) |
25 | | rabid 3326 |
. . . . 5
⊢ (𝑦 ∈ {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
26 | 24, 25 | syl6bbr 281 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 𝑦 ∈ {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅})) |
27 | 1, 2, 3, 26 | eqrd 3846 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) = {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅}) |
28 | | eqid 2825 |
. . . 4
⊢ (𝑦 ∈ ∪ 𝐾
↦ 〈𝐴, 𝑦〉) = (𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) |
29 | 28 | mptpreima 5869 |
. . 3
⊢ (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) = {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} |
30 | 27, 29 | syl6eqr 2879 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) = (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅)) |
31 | 9 | toptopon 21092 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
32 | 31 | biimpi 208 |
. . . . 5
⊢ (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
33 | 32 | ad2antlr 720 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
34 | 8 | toptopon 21092 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
35 | 34 | biimpi 208 |
. . . . . 6
⊢ (𝐽 ∈ Top → 𝐽 ∈ (TopOn‘𝑋)) |
36 | 35 | ad2antrr 719 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋)) |
37 | | simprr 791 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋) |
38 | 33, 36, 37 | cnmptc 21836 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) |
39 | 33 | cnmptid 21835 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 𝑦) ∈ (𝐾 Cn 𝐾)) |
40 | 33, 38, 39 | cnmpt1t 21839 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) ∈ (𝐾 Cn (𝐽 ×t 𝐾))) |
41 | | cnclima 21443 |
. . 3
⊢ (((𝑦 ∈ ∪ 𝐾
↦ 〈𝐴, 𝑦〉) ∈ (𝐾 Cn (𝐽 ×t 𝐾)) ∧ 𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾))) → (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) ∈ (Clsd‘𝐾)) |
42 | 40, 4, 41 | syl2anc 581 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) ∈ (Clsd‘𝐾)) |
43 | 30, 42 | eqeltrd 2906 |
1
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ (Clsd‘𝐾)) |