Step | Hyp | Ref
| Expression |
1 | | txcnmpt.1 |
. . . . . . 7
⊢ 𝑊 = ∪
𝑈 |
2 | | eqid 2610 |
. . . . . . 7
⊢ ∪ 𝑅 =
∪ 𝑅 |
3 | 1, 2 | cnf 20860 |
. . . . . 6
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝐹:𝑊⟶∪ 𝑅) |
4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐹:𝑊⟶∪ 𝑅) |
5 | 4 | ffvelrnda 6267 |
. . . 4
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝐹‘𝑥) ∈ ∪ 𝑅) |
6 | | eqid 2610 |
. . . . . . 7
⊢ ∪ 𝑆 =
∪ 𝑆 |
7 | 1, 6 | cnf 20860 |
. . . . . 6
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝐺:𝑊⟶∪ 𝑆) |
8 | 7 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐺:𝑊⟶∪ 𝑆) |
9 | 8 | ffvelrnda 6267 |
. . . 4
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝐺‘𝑥) ∈ ∪ 𝑆) |
10 | | opelxpi 5072 |
. . . 4
⊢ (((𝐹‘𝑥) ∈ ∪ 𝑅 ∧ (𝐺‘𝑥) ∈ ∪ 𝑆) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (∪
𝑅 × ∪ 𝑆)) |
11 | 5, 9, 10 | syl2anc 691 |
. . 3
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ 𝑥 ∈ 𝑊) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (∪
𝑅 × ∪ 𝑆)) |
12 | | txcnmpt.2 |
. . 3
⊢ 𝐻 = (𝑥 ∈ 𝑊 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
13 | 11, 12 | fmptd 6292 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐻:𝑊⟶(∪ 𝑅 × ∪ 𝑆)) |
14 | 12 | mptpreima 5545 |
. . . . . 6
⊢ (◡𝐻 “ (𝑟 × 𝑠)) = {𝑥 ∈ 𝑊 ∣ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠)} |
15 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐹:𝑊⟶∪ 𝑅) |
16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → 𝐹:𝑊⟶∪ 𝑅) |
17 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑊⟶∪ 𝑅 → 𝐹 Fn 𝑊) |
18 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝑊 → (𝑥 ∈ (◡𝐹 “ 𝑟) ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐹 “ 𝑟) ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
20 | | ibar 524 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑊 → ((𝐹‘𝑥) ∈ 𝑟 ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
21 | 20 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → ((𝐹‘𝑥) ∈ 𝑟 ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
22 | 19, 21 | bitr4d 270 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐹 “ 𝑟) ↔ (𝐹‘𝑥) ∈ 𝑟)) |
23 | 8 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → 𝐺:𝑊⟶∪ 𝑆) |
24 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐺:𝑊⟶∪ 𝑆 → 𝐺 Fn 𝑊) |
25 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn 𝑊 → (𝑥 ∈ (◡𝐺 “ 𝑠) ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐺 “ 𝑠) ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
27 | | ibar 524 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑊 → ((𝐺‘𝑥) ∈ 𝑠 ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
28 | 27 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → ((𝐺‘𝑥) ∈ 𝑠 ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
29 | 26, 28 | bitr4d 270 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐺 “ 𝑠) ↔ (𝐺‘𝑥) ∈ 𝑠)) |
30 | 22, 29 | anbi12d 743 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → ((𝑥 ∈ (◡𝐹 “ 𝑟) ∧ 𝑥 ∈ (◡𝐺 “ 𝑠)) ↔ ((𝐹‘𝑥) ∈ 𝑟 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
31 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ↔ (𝑥 ∈ (◡𝐹 “ 𝑟) ∧ 𝑥 ∈ (◡𝐺 “ 𝑠))) |
32 | | opelxp 5070 |
. . . . . . . . 9
⊢
(〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠) ↔ ((𝐹‘𝑥) ∈ 𝑟 ∧ (𝐺‘𝑥) ∈ 𝑠)) |
33 | 30, 31, 32 | 3bitr4g 302 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ↔ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠))) |
34 | 33 | rabbi2dva 3783 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑊 ∩ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) = {𝑥 ∈ 𝑊 ∣ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠)}) |
35 | | inss1 3795 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ (◡𝐹 “ 𝑟) |
36 | | cnvimass 5404 |
. . . . . . . . . 10
⊢ (◡𝐹 “ 𝑟) ⊆ dom 𝐹 |
37 | 35, 36 | sstri 3577 |
. . . . . . . . 9
⊢ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ dom 𝐹 |
38 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐹:𝑊⟶∪ 𝑅 → dom 𝐹 = 𝑊) |
39 | 15, 38 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → dom 𝐹 = 𝑊) |
40 | 37, 39 | syl5sseq 3616 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ 𝑊) |
41 | | sseqin2 3779 |
. . . . . . . 8
⊢ (((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ 𝑊 ↔ (𝑊 ∩ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
42 | 40, 41 | sylib 207 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑊 ∩ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
43 | 34, 42 | eqtr3d 2646 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → {𝑥 ∈ 𝑊 ∣ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠)} = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
44 | 14, 43 | syl5eq 2656 |
. . . . 5
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐻 “ (𝑟 × 𝑠)) = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
45 | | cntop1 20854 |
. . . . . . . 8
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑈 ∈ Top) |
46 | 45 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝑈 ∈ Top) |
47 | 46 | adantr 480 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑈 ∈ Top) |
48 | | cnima 20879 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝑟 ∈ 𝑅) → (◡𝐹 “ 𝑟) ∈ 𝑈) |
49 | 48 | ad2ant2r 779 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐹 “ 𝑟) ∈ 𝑈) |
50 | | cnima 20879 |
. . . . . . 7
⊢ ((𝐺 ∈ (𝑈 Cn 𝑆) ∧ 𝑠 ∈ 𝑆) → (◡𝐺 “ 𝑠) ∈ 𝑈) |
51 | 50 | ad2ant2l 778 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐺 “ 𝑠) ∈ 𝑈) |
52 | | inopn 20529 |
. . . . . 6
⊢ ((𝑈 ∈ Top ∧ (◡𝐹 “ 𝑟) ∈ 𝑈 ∧ (◡𝐺 “ 𝑠) ∈ 𝑈) → ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ∈ 𝑈) |
53 | 47, 49, 51, 52 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ∈ 𝑈) |
54 | 44, 53 | eqeltrd 2688 |
. . . 4
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈) |
55 | 54 | ralrimivva 2954 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∀𝑟 ∈ 𝑅 ∀𝑠 ∈ 𝑆 (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈) |
56 | | vex 3176 |
. . . . . 6
⊢ 𝑟 ∈ V |
57 | | vex 3176 |
. . . . . 6
⊢ 𝑠 ∈ V |
58 | 56, 57 | xpex 6860 |
. . . . 5
⊢ (𝑟 × 𝑠) ∈ V |
59 | 58 | rgen2w 2909 |
. . . 4
⊢
∀𝑟 ∈
𝑅 ∀𝑠 ∈ 𝑆 (𝑟 × 𝑠) ∈ V |
60 | | eqid 2610 |
. . . . 5
⊢ (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) = (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) |
61 | | imaeq2 5381 |
. . . . . 6
⊢ (𝑧 = (𝑟 × 𝑠) → (◡𝐻 “ 𝑧) = (◡𝐻 “ (𝑟 × 𝑠))) |
62 | 61 | eleq1d 2672 |
. . . . 5
⊢ (𝑧 = (𝑟 × 𝑠) → ((◡𝐻 “ 𝑧) ∈ 𝑈 ↔ (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈)) |
63 | 60, 62 | ralrnmpt2 6673 |
. . . 4
⊢
(∀𝑟 ∈
𝑅 ∀𝑠 ∈ 𝑆 (𝑟 × 𝑠) ∈ V → (∀𝑧 ∈ ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈 ↔ ∀𝑟 ∈ 𝑅 ∀𝑠 ∈ 𝑆 (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈)) |
64 | 59, 63 | ax-mp 5 |
. . 3
⊢
(∀𝑧 ∈
ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈 ↔ ∀𝑟 ∈ 𝑅 ∀𝑠 ∈ 𝑆 (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈) |
65 | 55, 64 | sylibr 223 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∀𝑧 ∈ ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈) |
66 | 1 | toptopon 20548 |
. . . 4
⊢ (𝑈 ∈ Top ↔ 𝑈 ∈ (TopOn‘𝑊)) |
67 | 46, 66 | sylib 207 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝑈 ∈ (TopOn‘𝑊)) |
68 | | cntop2 20855 |
. . . 4
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑅 ∈ Top) |
69 | | cntop2 20855 |
. . . 4
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑆 ∈ Top) |
70 | | eqid 2610 |
. . . . 5
⊢ ran
(𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) = ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) |
71 | 70 | txval 21177 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) = (topGen‘ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)))) |
72 | 68, 69, 71 | syl2an 493 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑅 ×t 𝑆) = (topGen‘ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)))) |
73 | 2 | toptopon 20548 |
. . . . 5
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) |
74 | 68, 73 | sylib 207 |
. . . 4
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑅 ∈ (TopOn‘∪ 𝑅)) |
75 | 6 | toptopon 20548 |
. . . . 5
⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆)) |
76 | 69, 75 | sylib 207 |
. . . 4
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑆 ∈ (TopOn‘∪ 𝑆)) |
77 | | txtopon 21204 |
. . . 4
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
78 | 74, 76, 77 | syl2an 493 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
79 | 67, 72, 78 | tgcn 20866 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝐻 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ (𝐻:𝑊⟶(∪ 𝑅 × ∪ 𝑆)
∧ ∀𝑧 ∈ ran
(𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈))) |
80 | 13, 65, 79 | mpbir2and 959 |
1
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐻 ∈ (𝑈 Cn (𝑅 ×t 𝑆))) |