| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑦((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) |
| 2 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦(𝑅 “ {𝐴}) |
| 3 | | nfrab1 3457 |
. . . 4
⊢
Ⅎ𝑦{𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} |
| 4 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾))) |
| 5 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐽
×t 𝐾) =
∪ (𝐽 ×t 𝐾) |
| 6 | 5 | cldss 23037 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) → 𝑅 ⊆ ∪ (𝐽 ×t 𝐾)) |
| 7 | 4, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ⊆ ∪ (𝐽 ×t 𝐾)) |
| 8 | | imasnopn.1 |
. . . . . . . . . . . . 13
⊢ 𝑋 = ∪
𝐽 |
| 9 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐾 =
∪ 𝐾 |
| 10 | 8, 9 | txuni 23600 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × ∪ 𝐾) =
∪ (𝐽 ×t 𝐾)) |
| 11 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑋 × ∪ 𝐾) = ∪
(𝐽 ×t
𝐾)) |
| 12 | 7, 11 | sseqtrrd 4021 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ⊆ (𝑋 × ∪ 𝐾)) |
| 13 | | imass1 6119 |
. . . . . . . . . 10
⊢ (𝑅 ⊆ (𝑋 × ∪ 𝐾) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × ∪ 𝐾) “ {𝐴})) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × ∪ 𝐾) “ {𝐴})) |
| 15 | | xpimasn 6205 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑋 → ((𝑋 × ∪ 𝐾) “ {𝐴}) = ∪ 𝐾) |
| 16 | 15 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → ((𝑋 × ∪ 𝐾) “ {𝐴}) = ∪ 𝐾) |
| 17 | 14, 16 | sseqtrd 4020 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ⊆ ∪
𝐾) |
| 18 | 17 | sseld 3982 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) → 𝑦 ∈ ∪ 𝐾)) |
| 19 | 18 | pm4.71rd 562 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ (𝑅 “ {𝐴})))) |
| 20 | | elimasng 6107 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ V) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
| 21 | 20 | elvd 3486 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
| 22 | 21 | ad2antll 729 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
| 23 | 22 | anbi2d 630 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → ((𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ (𝑅 “ {𝐴})) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅))) |
| 24 | 19, 23 | bitrd 279 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅))) |
| 25 | | rabid 3458 |
. . . . 5
⊢ (𝑦 ∈ {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
| 26 | 24, 25 | bitr4di 289 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 𝑦 ∈ {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅})) |
| 27 | 1, 2, 3, 26 | eqrd 4003 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) = {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅}) |
| 28 | | eqid 2737 |
. . . 4
⊢ (𝑦 ∈ ∪ 𝐾
↦ 〈𝐴, 𝑦〉) = (𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) |
| 29 | 28 | mptpreima 6258 |
. . 3
⊢ (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) = {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} |
| 30 | 27, 29 | eqtr4di 2795 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) = (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅)) |
| 31 | 9 | toptopon 22923 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 32 | 31 | biimpi 216 |
. . . . 5
⊢ (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 33 | 32 | ad2antlr 727 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 34 | 8 | toptopon 22923 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
| 35 | 34 | biimpi 216 |
. . . . . 6
⊢ (𝐽 ∈ Top → 𝐽 ∈ (TopOn‘𝑋)) |
| 36 | 35 | ad2antrr 726 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋)) |
| 37 | | simprr 773 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋) |
| 38 | 33, 36, 37 | cnmptc 23670 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) |
| 39 | 33 | cnmptid 23669 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 𝑦) ∈ (𝐾 Cn 𝐾)) |
| 40 | 33, 38, 39 | cnmpt1t 23673 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) ∈ (𝐾 Cn (𝐽 ×t 𝐾))) |
| 41 | | cnclima 23276 |
. . 3
⊢ (((𝑦 ∈ ∪ 𝐾
↦ 〈𝐴, 𝑦〉) ∈ (𝐾 Cn (𝐽 ×t 𝐾)) ∧ 𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾))) → (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) ∈ (Clsd‘𝐾)) |
| 42 | 40, 4, 41 | syl2anc 584 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) ∈ (Clsd‘𝐾)) |
| 43 | 30, 42 | eqeltrd 2841 |
1
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ (Clsd‘𝐾)) |