Step | Hyp | Ref
| Expression |
1 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑦((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) |
2 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑦(𝑅 “ {𝐴}) |
3 | | nfrab1 3122 |
. . . 4
⊢
Ⅎ𝑦{𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} |
4 | | txtop 21372 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) ∈ Top) |
5 | 4 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝐽 ×t 𝐾) ∈ Top) |
6 | | simprl 794 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ∈ (𝐽 ×t 𝐾)) |
7 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐽
×t 𝐾) =
∪ (𝐽 ×t 𝐾) |
8 | 7 | eltopss 20712 |
. . . . . . . . . . . 12
⊢ (((𝐽 ×t 𝐾) ∈ Top ∧ 𝑅 ∈ (𝐽 ×t 𝐾)) → 𝑅 ⊆ ∪ (𝐽 ×t 𝐾)) |
9 | 5, 6, 8 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ⊆ ∪ (𝐽 ×t 𝐾)) |
10 | | imasnopn.1 |
. . . . . . . . . . . . 13
⊢ 𝑋 = ∪
𝐽 |
11 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐾 =
∪ 𝐾 |
12 | 10, 11 | txuni 21395 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × ∪ 𝐾) =
∪ (𝐽 ×t 𝐾)) |
13 | 12 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑋 × ∪ 𝐾) = ∪
(𝐽 ×t
𝐾)) |
14 | 9, 13 | sseqtr4d 3642 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → 𝑅 ⊆ (𝑋 × ∪ 𝐾)) |
15 | | imass1 5500 |
. . . . . . . . . 10
⊢ (𝑅 ⊆ (𝑋 × ∪ 𝐾) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × ∪ 𝐾) “ {𝐴})) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × ∪ 𝐾) “ {𝐴})) |
17 | | xpimasn 5579 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑋 → ((𝑋 × ∪ 𝐾) “ {𝐴}) = ∪ 𝐾) |
18 | 17 | ad2antll 765 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → ((𝑋 × ∪ 𝐾) “ {𝐴}) = ∪ 𝐾) |
19 | 16, 18 | sseqtrd 3641 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ⊆ ∪
𝐾) |
20 | 19 | sseld 3602 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) → 𝑦 ∈ ∪ 𝐾)) |
21 | 20 | pm4.71rd 667 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ (𝑅 “ {𝐴})))) |
22 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
23 | | elimasng 5491 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ V) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
24 | 22, 23 | mpan2 707 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
25 | 24 | ad2antll 765 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
26 | 25 | anbi2d 740 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → ((𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ (𝑅 “ {𝐴})) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅))) |
27 | 21, 26 | bitrd 268 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅))) |
28 | | rabid 3116 |
. . . . 5
⊢ (𝑦 ∈ {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} ↔ (𝑦 ∈ ∪ 𝐾 ∧ 〈𝐴, 𝑦〉 ∈ 𝑅)) |
29 | 27, 28 | syl6bbr 278 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 𝑦 ∈ {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅})) |
30 | 1, 2, 3, 29 | eqrd 3622 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) = {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅}) |
31 | | eqid 2622 |
. . . 4
⊢ (𝑦 ∈ ∪ 𝐾
↦ 〈𝐴, 𝑦〉) = (𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) |
32 | 31 | mptpreima 5628 |
. . 3
⊢ (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) = {𝑦 ∈ ∪ 𝐾 ∣ 〈𝐴, 𝑦〉 ∈ 𝑅} |
33 | 30, 32 | syl6eqr 2674 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) = (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅)) |
34 | 11 | toptopon 20722 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
35 | 34 | biimpi 206 |
. . . . 5
⊢ (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
36 | 35 | ad2antlr 763 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
37 | 10 | toptopon 20722 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
38 | 37 | biimpi 206 |
. . . . . 6
⊢ (𝐽 ∈ Top → 𝐽 ∈ (TopOn‘𝑋)) |
39 | 38 | ad2antrr 762 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋)) |
40 | | simprr 796 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋) |
41 | 36, 39, 40 | cnmptc 21465 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) |
42 | 36 | cnmptid 21464 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 𝑦) ∈ (𝐾 Cn 𝐾)) |
43 | 36, 41, 42 | cnmpt1t 21468 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) ∈ (𝐾 Cn (𝐽 ×t 𝐾))) |
44 | | cnima 21069 |
. . 3
⊢ (((𝑦 ∈ ∪ 𝐾
↦ 〈𝐴, 𝑦〉) ∈ (𝐾 Cn (𝐽 ×t 𝐾)) ∧ 𝑅 ∈ (𝐽 ×t 𝐾)) → (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) ∈ 𝐾) |
45 | 43, 6, 44 | syl2anc 693 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (◡(𝑦 ∈ ∪ 𝐾 ↦ 〈𝐴, 𝑦〉) “ 𝑅) ∈ 𝐾) |
46 | 33, 45 | eqeltrd 2701 |
1
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ 𝐾) |