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