Step | Hyp | Ref
| Expression |
1 | | txcnmpt.1 |
. . . . . . 7
⊢ 𝑊 = ∪
𝑈 |
2 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝑅 =
∪ 𝑅 |
3 | 1, 2 | cnf 21050 |
. . . . . 6
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝐹:𝑊⟶∪ 𝑅) |
4 | 3 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐹:𝑊⟶∪ 𝑅) |
5 | 4 | ffvelrnda 6359 |
. . . 4
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝐹‘𝑥) ∈ ∪ 𝑅) |
6 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝑆 =
∪ 𝑆 |
7 | 1, 6 | cnf 21050 |
. . . . . 6
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝐺:𝑊⟶∪ 𝑆) |
8 | 7 | adantl 482 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐺:𝑊⟶∪ 𝑆) |
9 | 8 | ffvelrnda 6359 |
. . . 4
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝐺‘𝑥) ∈ ∪ 𝑆) |
10 | | opelxpi 5148 |
. . . 4
⊢ (((𝐹‘𝑥) ∈ ∪ 𝑅 ∧ (𝐺‘𝑥) ∈ ∪ 𝑆) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (∪
𝑅 × ∪ 𝑆)) |
11 | 5, 9, 10 | syl2anc 693 |
. . 3
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ 𝑥 ∈ 𝑊) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (∪
𝑅 × ∪ 𝑆)) |
12 | | txcnmpt.2 |
. . 3
⊢ 𝐻 = (𝑥 ∈ 𝑊 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
13 | 11, 12 | fmptd 6385 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐻:𝑊⟶(∪ 𝑅 × ∪ 𝑆)) |
14 | 12 | mptpreima 5628 |
. . . . . 6
⊢ (◡𝐻 “ (𝑟 × 𝑠)) = {𝑥 ∈ 𝑊 ∣ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠)} |
15 | 4 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐹:𝑊⟶∪ 𝑅) |
16 | 15 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → 𝐹:𝑊⟶∪ 𝑅) |
17 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑊⟶∪ 𝑅 → 𝐹 Fn 𝑊) |
18 | | elpreima 6337 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝑊 → (𝑥 ∈ (◡𝐹 “ 𝑟) ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐹 “ 𝑟) ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
20 | | ibar 525 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑊 → ((𝐹‘𝑥) ∈ 𝑟 ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
21 | 20 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → ((𝐹‘𝑥) ∈ 𝑟 ↔ (𝑥 ∈ 𝑊 ∧ (𝐹‘𝑥) ∈ 𝑟))) |
22 | 19, 21 | bitr4d 271 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐹 “ 𝑟) ↔ (𝐹‘𝑥) ∈ 𝑟)) |
23 | 8 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → 𝐺:𝑊⟶∪ 𝑆) |
24 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝐺:𝑊⟶∪ 𝑆 → 𝐺 Fn 𝑊) |
25 | | elpreima 6337 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn 𝑊 → (𝑥 ∈ (◡𝐺 “ 𝑠) ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐺 “ 𝑠) ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
27 | | ibar 525 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑊 → ((𝐺‘𝑥) ∈ 𝑠 ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
28 | 27 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → ((𝐺‘𝑥) ∈ 𝑠 ↔ (𝑥 ∈ 𝑊 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
29 | 26, 28 | bitr4d 271 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ (◡𝐺 “ 𝑠) ↔ (𝐺‘𝑥) ∈ 𝑠)) |
30 | 22, 29 | anbi12d 747 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → ((𝑥 ∈ (◡𝐹 “ 𝑟) ∧ 𝑥 ∈ (◡𝐺 “ 𝑠)) ↔ ((𝐹‘𝑥) ∈ 𝑟 ∧ (𝐺‘𝑥) ∈ 𝑠))) |
31 | | elin 3796 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ↔ (𝑥 ∈ (◡𝐹 “ 𝑟) ∧ 𝑥 ∈ (◡𝐺 “ 𝑠))) |
32 | | opelxp 5146 |
. . . . . . . . 9
⊢
(〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠) ↔ ((𝐹‘𝑥) ∈ 𝑟 ∧ (𝐺‘𝑥) ∈ 𝑠)) |
33 | 30, 31, 32 | 3bitr4g 303 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ↔ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠))) |
34 | 33 | rabbi2dva 3821 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑊 ∩ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) = {𝑥 ∈ 𝑊 ∣ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠)}) |
35 | | inss1 3833 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ (◡𝐹 “ 𝑟) |
36 | | cnvimass 5485 |
. . . . . . . . . 10
⊢ (◡𝐹 “ 𝑟) ⊆ dom 𝐹 |
37 | 35, 36 | sstri 3612 |
. . . . . . . . 9
⊢ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ dom 𝐹 |
38 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝑊⟶∪ 𝑅 → dom 𝐹 = 𝑊) |
39 | 15, 38 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → dom 𝐹 = 𝑊) |
40 | 37, 39 | syl5sseq 3653 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ 𝑊) |
41 | | sseqin2 3817 |
. . . . . . . 8
⊢ (((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ⊆ 𝑊 ↔ (𝑊 ∩ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
42 | 40, 41 | sylib 208 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑊 ∩ ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
43 | 34, 42 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → {𝑥 ∈ 𝑊 ∣ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑟 × 𝑠)} = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
44 | 14, 43 | syl5eq 2668 |
. . . . 5
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐻 “ (𝑟 × 𝑠)) = ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠))) |
45 | | cntop1 21044 |
. . . . . . . 8
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑈 ∈ Top) |
46 | 45 | adantl 482 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝑈 ∈ Top) |
47 | 46 | adantr 481 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑈 ∈ Top) |
48 | | cnima 21069 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝑟 ∈ 𝑅) → (◡𝐹 “ 𝑟) ∈ 𝑈) |
49 | 48 | ad2ant2r 783 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐹 “ 𝑟) ∈ 𝑈) |
50 | | cnima 21069 |
. . . . . . 7
⊢ ((𝐺 ∈ (𝑈 Cn 𝑆) ∧ 𝑠 ∈ 𝑆) → (◡𝐺 “ 𝑠) ∈ 𝑈) |
51 | 50 | ad2ant2l 782 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐺 “ 𝑠) ∈ 𝑈) |
52 | | inopn 20704 |
. . . . . 6
⊢ ((𝑈 ∈ Top ∧ (◡𝐹 “ 𝑟) ∈ 𝑈 ∧ (◡𝐺 “ 𝑠) ∈ 𝑈) → ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ∈ 𝑈) |
53 | 47, 49, 51, 52 | syl3anc 1326 |
. . . . 5
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((◡𝐹 “ 𝑟) ∩ (◡𝐺 “ 𝑠)) ∈ 𝑈) |
54 | 44, 53 | eqeltrd 2701 |
. . . 4
⊢ (((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈) |
55 | 54 | ralrimivva 2971 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∀𝑟 ∈ 𝑅 ∀𝑠 ∈ 𝑆 (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈) |
56 | | vex 3203 |
. . . . . 6
⊢ 𝑟 ∈ V |
57 | | vex 3203 |
. . . . . 6
⊢ 𝑠 ∈ V |
58 | 56, 57 | xpex 6962 |
. . . . 5
⊢ (𝑟 × 𝑠) ∈ V |
59 | 58 | rgen2w 2925 |
. . . 4
⊢
∀𝑟 ∈
𝑅 ∀𝑠 ∈ 𝑆 (𝑟 × 𝑠) ∈ V |
60 | | eqid 2622 |
. . . . 5
⊢ (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) = (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) |
61 | | imaeq2 5462 |
. . . . . 6
⊢ (𝑧 = (𝑟 × 𝑠) → (◡𝐻 “ 𝑧) = (◡𝐻 “ (𝑟 × 𝑠))) |
62 | 61 | eleq1d 2686 |
. . . . 5
⊢ (𝑧 = (𝑟 × 𝑠) → ((◡𝐻 “ 𝑧) ∈ 𝑈 ↔ (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈)) |
63 | 60, 62 | ralrnmpt2 6775 |
. . . 4
⊢
(∀𝑟 ∈
𝑅 ∀𝑠 ∈ 𝑆 (𝑟 × 𝑠) ∈ V → (∀𝑧 ∈ ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈 ↔ ∀𝑟 ∈ 𝑅 ∀𝑠 ∈ 𝑆 (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈)) |
64 | 59, 63 | ax-mp 5 |
. . 3
⊢
(∀𝑧 ∈
ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈 ↔ ∀𝑟 ∈ 𝑅 ∀𝑠 ∈ 𝑆 (◡𝐻 “ (𝑟 × 𝑠)) ∈ 𝑈) |
65 | 55, 64 | sylibr 224 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∀𝑧 ∈ ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈) |
66 | 1 | toptopon 20722 |
. . . 4
⊢ (𝑈 ∈ Top ↔ 𝑈 ∈ (TopOn‘𝑊)) |
67 | 46, 66 | sylib 208 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝑈 ∈ (TopOn‘𝑊)) |
68 | | cntop2 21045 |
. . . 4
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑅 ∈ Top) |
69 | | cntop2 21045 |
. . . 4
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑆 ∈ Top) |
70 | | eqid 2622 |
. . . . 5
⊢ ran
(𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) = ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)) |
71 | 70 | txval 21367 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) = (topGen‘ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)))) |
72 | 68, 69, 71 | syl2an 494 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑅 ×t 𝑆) = (topGen‘ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠)))) |
73 | 2 | toptopon 20722 |
. . . . 5
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) |
74 | 68, 73 | sylib 208 |
. . . 4
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑅 ∈ (TopOn‘∪ 𝑅)) |
75 | 6 | toptopon 20722 |
. . . . 5
⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆)) |
76 | 69, 75 | sylib 208 |
. . . 4
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑆 ∈ (TopOn‘∪ 𝑆)) |
77 | | txtopon 21394 |
. . . 4
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
78 | 74, 76, 77 | syl2an 494 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
79 | 67, 72, 78 | tgcn 21056 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝐻 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ (𝐻:𝑊⟶(∪ 𝑅 × ∪ 𝑆)
∧ ∀𝑧 ∈ ran
(𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (𝑟 × 𝑠))(◡𝐻 “ 𝑧) ∈ 𝑈))) |
80 | 13, 65, 79 | mpbir2and 957 |
1
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐻 ∈ (𝑈 Cn (𝑅 ×t 𝑆))) |