Step | Hyp | Ref
| Expression |
1 | | cnconst2 20897 |
. . . 4
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌) ∧ 𝑥 ∈ 𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆)) |
2 | 1 | 3expa 1257 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆)) |
3 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) = (𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) |
4 | 2, 3 | fmptd 6292 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})):𝑌⟶(𝑅 Cn 𝑆)) |
5 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
6 | | eqid 2610 |
. . . . . 6
⊢ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp} = {𝑧 ∈
𝒫 ∪ 𝑅 ∣ (𝑅 ↾t 𝑧) ∈ Comp} |
7 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
8 | 5, 6, 7 | xkobval 21199 |
. . . . 5
⊢ ran
(𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑦 ∣ ∃𝑘 ∈ 𝒫 ∪ 𝑅∃𝑣 ∈ 𝑆 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})} |
9 | 8 | abeq2i 2722 |
. . . 4
⊢ (𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ↔ ∃𝑘 ∈ 𝒫 ∪ 𝑅∃𝑣 ∈ 𝑆 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
10 | 2 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆)) |
11 | 10 | adantlr 747 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑥 ∈ 𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆)) |
12 | 11 | adantlr 747 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥 ∈ 𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆)) |
13 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥 ∈ 𝑌) → 𝑘 = ∅) |
14 | 13 | imaeq2d 5385 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥 ∈ 𝑌) → ((𝑋 × {𝑥}) “ 𝑘) = ((𝑋 × {𝑥}) “ ∅)) |
15 | | ima0 5400 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 × {𝑥}) “ ∅) =
∅ |
16 | | 0ss 3924 |
. . . . . . . . . . . . . 14
⊢ ∅
⊆ 𝑣 |
17 | 15, 16 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢ ((𝑋 × {𝑥}) “ ∅) ⊆ 𝑣 |
18 | 14, 17 | syl6eqss 3618 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥 ∈ 𝑌) → ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣) |
19 | | imaeq1 5380 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑋 × {𝑥}) → (𝑓 “ 𝑘) = ((𝑋 × {𝑥}) “ 𝑘)) |
20 | 19 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑋 × {𝑥}) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣)) |
21 | 20 | elrab 3331 |
. . . . . . . . . . . 12
⊢ ((𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣)) |
22 | 12, 18, 21 | sylanbrc 695 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥 ∈ 𝑌) → (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
23 | 22 | ralrimiva 2949 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → ∀𝑥 ∈ 𝑌 (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
24 | | rabid2 3096 |
. . . . . . . . . 10
⊢ (𝑌 = {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ↔ ∀𝑥 ∈ 𝑌 (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
25 | 23, 24 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → 𝑌 = {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}) |
26 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑆 ∈ (TopOn‘𝑌)) |
27 | | toponmax 20543 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝑆) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑌 ∈ 𝑆) |
29 | 28 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → 𝑌 ∈ 𝑆) |
30 | 25, 29 | eqeltrrd 2689 |
. . . . . . . 8
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ∈ 𝑆) |
31 | | ifnefalse 4048 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ≠ ∅ → if(𝑘 = ∅, 𝑌, 𝑣) = 𝑣) |
32 | 31 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → if(𝑘 = ∅, 𝑌, 𝑣) = 𝑣) |
33 | 32 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ if(𝑘 = ∅, 𝑌, 𝑣) ↔ 𝑥 ∈ 𝑣)) |
34 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
35 | 34 | snss 4259 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑣 ↔ {𝑥} ⊆ 𝑣) |
36 | 33, 35 | syl6bb 275 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ if(𝑘 = ∅, 𝑌, 𝑣) ↔ {𝑥} ⊆ 𝑣)) |
37 | | df-ima 5051 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 × {𝑥}) “ 𝑘) = ran ((𝑋 × {𝑥}) ↾ 𝑘) |
38 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑘 ∈ 𝒫 ∪ 𝑅) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → 𝑘 ∈ 𝒫 ∪ 𝑅) |
40 | 39 | elpwid 4118 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → 𝑘 ⊆ ∪ 𝑅) |
41 | | toponuni 20542 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅) |
42 | 41 | ad5antr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → 𝑋 = ∪ 𝑅) |
43 | 40, 42 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → 𝑘 ⊆ 𝑋) |
44 | | xpssres 5354 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ⊆ 𝑋 → ((𝑋 × {𝑥}) ↾ 𝑘) = (𝑘 × {𝑥})) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → ((𝑋 × {𝑥}) ↾ 𝑘) = (𝑘 × {𝑥})) |
46 | 45 | rneqd 5274 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → ran ((𝑋 × {𝑥}) ↾ 𝑘) = ran (𝑘 × {𝑥})) |
47 | 37, 46 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → ((𝑋 × {𝑥}) “ 𝑘) = ran (𝑘 × {𝑥})) |
48 | | rnxp 5483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ≠ ∅ → ran (𝑘 × {𝑥}) = {𝑥}) |
49 | 48 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → ran (𝑘 × {𝑥}) = {𝑥}) |
50 | 47, 49 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → ((𝑋 × {𝑥}) “ 𝑘) = {𝑥}) |
51 | 50 | sseq1d 3595 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣 ↔ {𝑥} ⊆ 𝑣)) |
52 | 11 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆)) |
53 | 52 | biantrurd 528 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣 ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣))) |
54 | 36, 51, 53 | 3bitr2d 295 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ if(𝑘 = ∅, 𝑌, 𝑣) ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣))) |
55 | 33, 54 | bitr3d 269 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ 𝑣 ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣))) |
56 | 55, 21 | syl6bbr 277 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ 𝑣 ↔ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
57 | 56 | rabbi2dva 3783 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → (𝑌 ∩ 𝑣) = {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}) |
58 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑣 ∈ 𝑆) |
59 | | toponss 20544 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ (TopOn‘𝑌) ∧ 𝑣 ∈ 𝑆) → 𝑣 ⊆ 𝑌) |
60 | 26, 58, 59 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑣 ⊆ 𝑌) |
61 | 60 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → 𝑣 ⊆ 𝑌) |
62 | | sseqin2 3779 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ 𝑌 ↔ (𝑌 ∩ 𝑣) = 𝑣) |
63 | 61, 62 | sylib 207 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → (𝑌 ∩ 𝑣) = 𝑣) |
64 | 57, 63 | eqtr3d 2646 |
. . . . . . . . 9
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} = 𝑣) |
65 | 58 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → 𝑣 ∈ 𝑆) |
66 | 64, 65 | eqeltrd 2688 |
. . . . . . . 8
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ∈ 𝑆) |
67 | 30, 66 | pm2.61dane 2869 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ∈ 𝑆) |
68 | | imaeq2 5381 |
. . . . . . . . 9
⊢ (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) = (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
69 | 3 | mptpreima 5545 |
. . . . . . . . 9
⊢ (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} |
70 | 68, 69 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) = {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}) |
71 | 70 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → ((◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆 ↔ {𝑥 ∈ 𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ∈ 𝑆)) |
72 | 67, 71 | syl5ibrcom 236 |
. . . . . 6
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆)) |
73 | 72 | expimpd 627 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑆)) → (((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) → (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆)) |
74 | 73 | rexlimdvva 3020 |
. . . 4
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (∃𝑘 ∈ 𝒫 ∪ 𝑅∃𝑣 ∈ 𝑆 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) → (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆)) |
75 | 9, 74 | syl5bi 231 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) → (◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆)) |
76 | 75 | ralrimiv 2948 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ∀𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})(◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆) |
77 | | simpr 476 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑆 ∈ (TopOn‘𝑌)) |
78 | | ovex 6577 |
. . . . . 6
⊢ (𝑅 Cn 𝑆) ∈ V |
79 | 78 | pwex 4774 |
. . . . 5
⊢ 𝒫
(𝑅 Cn 𝑆) ∈ V |
80 | 5, 6, 7 | xkotf 21198 |
. . . . . 6
⊢ (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}):({𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) |
81 | | frn 5966 |
. . . . . 6
⊢ ((𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}):({𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) → ran (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆)) |
82 | 80, 81 | ax-mp 5 |
. . . . 5
⊢ ran
(𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆) |
83 | 79, 82 | ssexi 4731 |
. . . 4
⊢ ran
(𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ∈ V |
84 | 83 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ran (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ∈ V) |
85 | | topontop 20541 |
. . . 4
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top) |
86 | | topontop 20541 |
. . . 4
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top) |
87 | 5, 6, 7 | xkoval 21200 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) = (topGen‘(fi‘ran
(𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
88 | 85, 86, 87 | syl2an 493 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑆 ^ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
89 | | eqid 2610 |
. . . . 5
⊢ (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅) |
90 | 89 | xkotopon 21213 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆))) |
91 | 85, 86, 90 | syl2an 493 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑆 ^ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆))) |
92 | 77, 84, 88, 91 | subbascn 20868 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ((𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) ∈ (𝑆 Cn (𝑆 ^ko 𝑅)) ↔ ((𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})):𝑌⟶(𝑅 Cn 𝑆) ∧ ∀𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑧)
∈ Comp}, 𝑣 ∈
𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})(◡(𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆))) |
93 | 4, 76, 92 | mpbir2and 959 |
1
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) ∈ (𝑆 Cn (𝑆 ^ko 𝑅))) |