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