Step |
Hyp |
Ref |
Expression |
1 |
|
haustop |
⊢ ( 𝑅 ∈ Haus → 𝑅 ∈ Top ) |
2 |
|
haustop |
⊢ ( 𝑆 ∈ Haus → 𝑆 ∈ Top ) |
3 |
|
txtop |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑅 ×t 𝑆 ) ∈ Top ) |
5 |
|
eqid |
⊢ ∪ 𝑅 = ∪ 𝑅 |
6 |
|
eqid |
⊢ ∪ 𝑆 = ∪ 𝑆 |
7 |
5 6
|
txuni |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
8 |
1 2 7
|
syl2an |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
9 |
8
|
eleq2d |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ↔ 𝑥 ∈ ∪ ( 𝑅 ×t 𝑆 ) ) ) |
10 |
8
|
eleq2d |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ↔ 𝑦 ∈ ∪ ( 𝑅 ×t 𝑆 ) ) ) |
11 |
9 10
|
anbi12d |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ↔ ( 𝑥 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∧ 𝑦 ∈ ∪ ( 𝑅 ×t 𝑆 ) ) ) ) |
12 |
|
neorian |
⊢ ( ( ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ↔ ¬ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) |
13 |
|
xpopth |
⊢ ( ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) → ( ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) ) |
15 |
14
|
necon3bbid |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ¬ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ↔ 𝑥 ≠ 𝑦 ) ) |
16 |
12 15
|
syl5bb |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ( ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ↔ 𝑥 ≠ 𝑦 ) ) |
17 |
|
simplll |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) → 𝑅 ∈ Haus ) |
18 |
|
xp1st |
⊢ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 1st ‘ 𝑥 ) ∈ ∪ 𝑅 ) |
19 |
18
|
ad2antrl |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 1st ‘ 𝑥 ) ∈ ∪ 𝑅 ) |
20 |
19
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) → ( 1st ‘ 𝑥 ) ∈ ∪ 𝑅 ) |
21 |
|
xp1st |
⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 ) |
22 |
21
|
ad2antll |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 ) |
23 |
22
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) → ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 ) |
24 |
|
simpr |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) → ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) |
25 |
5
|
hausnei |
⊢ ( ( 𝑅 ∈ Haus ∧ ( ( 1st ‘ 𝑥 ) ∈ ∪ 𝑅 ∧ ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑅 ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
26 |
17 20 23 24 25
|
syl13anc |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑅 ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
27 |
1
|
ad2antrr |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → 𝑅 ∈ Top ) |
28 |
27
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑅 ∈ Top ) |
29 |
2
|
ad4antlr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑆 ∈ Top ) |
30 |
|
simprll |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑢 ∈ 𝑅 ) |
31 |
6
|
topopn |
⊢ ( 𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆 ) |
32 |
29 31
|
syl |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∪ 𝑆 ∈ 𝑆 ) |
33 |
|
txopn |
⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑢 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆 ) ) → ( 𝑢 × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
34 |
28 29 30 32 33
|
syl22anc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑢 × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
35 |
|
simprlr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑣 ∈ 𝑅 ) |
36 |
|
txopn |
⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑣 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆 ) ) → ( 𝑣 × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
37 |
28 29 35 32 36
|
syl22anc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑣 × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
38 |
|
1st2nd2 |
⊢ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ) |
39 |
38
|
ad2antrl |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ) |
40 |
39
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ) |
41 |
|
simprr1 |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1st ‘ 𝑥 ) ∈ 𝑢 ) |
42 |
|
xp2nd |
⊢ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 2nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) |
43 |
42
|
ad2antrl |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 2nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) |
44 |
43
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) |
45 |
41 44
|
jca |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) ) |
46 |
|
elxp6 |
⊢ ( 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ↔ ( 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) ) ) |
47 |
40 45 46
|
sylanbrc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ) |
48 |
|
1st2nd2 |
⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ) |
49 |
48
|
ad2antll |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ) |
50 |
49
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ) |
51 |
|
simprr2 |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1st ‘ 𝑦 ) ∈ 𝑣 ) |
52 |
|
xp2nd |
⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) |
53 |
52
|
ad2antll |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) |
54 |
53
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) |
55 |
51 54
|
jca |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) ) |
56 |
|
elxp6 |
⊢ ( 𝑦 ∈ ( 𝑣 × ∪ 𝑆 ) ↔ ( 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) ) ) |
57 |
50 55 56
|
sylanbrc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ( 𝑣 × ∪ 𝑆 ) ) |
58 |
|
simprr3 |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑢 ∩ 𝑣 ) = ∅ ) |
59 |
58
|
xpeq1d |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 𝑢 ∩ 𝑣 ) × ∪ 𝑆 ) = ( ∅ × ∪ 𝑆 ) ) |
60 |
|
xpindir |
⊢ ( ( 𝑢 ∩ 𝑣 ) × ∪ 𝑆 ) = ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) ) |
61 |
|
0xp |
⊢ ( ∅ × ∪ 𝑆 ) = ∅ |
62 |
59 60 61
|
3eqtr3g |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) ) = ∅ ) |
63 |
|
eleq2 |
⊢ ( 𝑧 = ( 𝑢 × ∪ 𝑆 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ) ) |
64 |
|
ineq1 |
⊢ ( 𝑧 = ( 𝑢 × ∪ 𝑆 ) → ( 𝑧 ∩ 𝑤 ) = ( ( 𝑢 × ∪ 𝑆 ) ∩ 𝑤 ) ) |
65 |
64
|
eqeq1d |
⊢ ( 𝑧 = ( 𝑢 × ∪ 𝑆 ) → ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ( ( 𝑢 × ∪ 𝑆 ) ∩ 𝑤 ) = ∅ ) ) |
66 |
63 65
|
3anbi13d |
⊢ ( 𝑧 = ( 𝑢 × ∪ 𝑆 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ∧ 𝑦 ∈ 𝑤 ∧ ( ( 𝑢 × ∪ 𝑆 ) ∩ 𝑤 ) = ∅ ) ) ) |
67 |
|
eleq2 |
⊢ ( 𝑤 = ( 𝑣 × ∪ 𝑆 ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( 𝑣 × ∪ 𝑆 ) ) ) |
68 |
|
ineq2 |
⊢ ( 𝑤 = ( 𝑣 × ∪ 𝑆 ) → ( ( 𝑢 × ∪ 𝑆 ) ∩ 𝑤 ) = ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) ) ) |
69 |
68
|
eqeq1d |
⊢ ( 𝑤 = ( 𝑣 × ∪ 𝑆 ) → ( ( ( 𝑢 × ∪ 𝑆 ) ∩ 𝑤 ) = ∅ ↔ ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) ) = ∅ ) ) |
70 |
67 69
|
3anbi23d |
⊢ ( 𝑤 = ( 𝑣 × ∪ 𝑆 ) → ( ( 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ∧ 𝑦 ∈ 𝑤 ∧ ( ( 𝑢 × ∪ 𝑆 ) ∩ 𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( 𝑣 × ∪ 𝑆 ) ∧ ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) ) = ∅ ) ) ) |
71 |
66 70
|
rspc2ev |
⊢ ( ( ( 𝑢 × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑣 × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( 𝑣 × ∪ 𝑆 ) ∧ ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) ) = ∅ ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) |
72 |
34 37 47 57 62 71
|
syl113anc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) |
73 |
72
|
expr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ) → ( ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) |
74 |
73
|
rexlimdvva |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑅 ( ( 1st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) |
75 |
26 74
|
mpd |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) |
76 |
|
simpllr |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → 𝑆 ∈ Haus ) |
77 |
43
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → ( 2nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) |
78 |
53
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) |
79 |
|
simpr |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) |
80 |
6
|
hausnei |
⊢ ( ( 𝑆 ∈ Haus ∧ ( ( 2nd ‘ 𝑥 ) ∈ ∪ 𝑆 ∧ ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ 𝑆 ∃ 𝑣 ∈ 𝑆 ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
81 |
76 77 78 79 80
|
syl13anc |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑆 ∃ 𝑣 ∈ 𝑆 ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
82 |
27
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑅 ∈ Top ) |
83 |
2
|
ad4antlr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑆 ∈ Top ) |
84 |
5
|
topopn |
⊢ ( 𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅 ) |
85 |
82 84
|
syl |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∪ 𝑅 ∈ 𝑅 ) |
86 |
|
simprll |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑢 ∈ 𝑆 ) |
87 |
|
txopn |
⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( ∪ 𝑅 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) → ( ∪ 𝑅 × 𝑢 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
88 |
82 83 85 86 87
|
syl22anc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ∪ 𝑅 × 𝑢 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
89 |
|
simprlr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑣 ∈ 𝑆 ) |
90 |
|
txopn |
⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( ∪ 𝑅 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) → ( ∪ 𝑅 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
91 |
82 83 85 89 90
|
syl22anc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ∪ 𝑅 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
92 |
39
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ) |
93 |
19
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1st ‘ 𝑥 ) ∈ ∪ 𝑅 ) |
94 |
|
simprr1 |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2nd ‘ 𝑥 ) ∈ 𝑢 ) |
95 |
93 94
|
jca |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1st ‘ 𝑥 ) ∈ ∪ 𝑅 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝑢 ) ) |
96 |
|
elxp6 |
⊢ ( 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ↔ ( 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ∧ ( ( 1st ‘ 𝑥 ) ∈ ∪ 𝑅 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝑢 ) ) ) |
97 |
92 95 96
|
sylanbrc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ) |
98 |
49
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ) |
99 |
22
|
ad2antrr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 ) |
100 |
|
simprr2 |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2nd ‘ 𝑦 ) ∈ 𝑣 ) |
101 |
99 100
|
jca |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ) ) |
102 |
|
elxp6 |
⊢ ( 𝑦 ∈ ( ∪ 𝑅 × 𝑣 ) ↔ ( 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ∧ ( ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ) ) ) |
103 |
98 101 102
|
sylanbrc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ( ∪ 𝑅 × 𝑣 ) ) |
104 |
|
simprr3 |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑢 ∩ 𝑣 ) = ∅ ) |
105 |
104
|
xpeq2d |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ∪ 𝑅 × ( 𝑢 ∩ 𝑣 ) ) = ( ∪ 𝑅 × ∅ ) ) |
106 |
|
xpindi |
⊢ ( ∪ 𝑅 × ( 𝑢 ∩ 𝑣 ) ) = ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) ) |
107 |
|
xp0 |
⊢ ( ∪ 𝑅 × ∅ ) = ∅ |
108 |
105 106 107
|
3eqtr3g |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) ) = ∅ ) |
109 |
|
eleq2 |
⊢ ( 𝑧 = ( ∪ 𝑅 × 𝑢 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ) ) |
110 |
|
ineq1 |
⊢ ( 𝑧 = ( ∪ 𝑅 × 𝑢 ) → ( 𝑧 ∩ 𝑤 ) = ( ( ∪ 𝑅 × 𝑢 ) ∩ 𝑤 ) ) |
111 |
110
|
eqeq1d |
⊢ ( 𝑧 = ( ∪ 𝑅 × 𝑢 ) → ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ( ( ∪ 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ) ) |
112 |
109 111
|
3anbi13d |
⊢ ( 𝑧 = ( ∪ 𝑅 × 𝑢 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ∧ 𝑦 ∈ 𝑤 ∧ ( ( ∪ 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ) ) ) |
113 |
|
eleq2 |
⊢ ( 𝑤 = ( ∪ 𝑅 × 𝑣 ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( ∪ 𝑅 × 𝑣 ) ) ) |
114 |
|
ineq2 |
⊢ ( 𝑤 = ( ∪ 𝑅 × 𝑣 ) → ( ( ∪ 𝑅 × 𝑢 ) ∩ 𝑤 ) = ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) ) ) |
115 |
114
|
eqeq1d |
⊢ ( 𝑤 = ( ∪ 𝑅 × 𝑣 ) → ( ( ( ∪ 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ↔ ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) ) = ∅ ) ) |
116 |
113 115
|
3anbi23d |
⊢ ( 𝑤 = ( ∪ 𝑅 × 𝑣 ) → ( ( 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ∧ 𝑦 ∈ 𝑤 ∧ ( ( ∪ 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × 𝑣 ) ∧ ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) ) = ∅ ) ) ) |
117 |
112 116
|
rspc2ev |
⊢ ( ( ( ∪ 𝑅 × 𝑢 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( ∪ 𝑅 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × 𝑣 ) ∧ ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) ) = ∅ ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) |
118 |
88 91 97 103 108 117
|
syl113anc |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) |
119 |
118
|
expr |
⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) |
120 |
119
|
rexlimdvva |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ 𝑆 ∃ 𝑣 ∈ 𝑆 ( ( 2nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) |
121 |
81 120
|
mpd |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) |
122 |
75 121
|
jaodan |
⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) |
123 |
122
|
ex |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ( ( 1st ‘ 𝑥 ) ≠ ( 1st ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) ≠ ( 2nd ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) |
124 |
16 123
|
sylbird |
⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) |
125 |
124
|
ex |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) ) |
126 |
11 125
|
sylbird |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( ( 𝑥 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∧ 𝑦 ∈ ∪ ( 𝑅 ×t 𝑆 ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) ) |
127 |
126
|
ralrimivv |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ∀ 𝑥 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∀ 𝑦 ∈ ∪ ( 𝑅 ×t 𝑆 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) |
128 |
|
eqid |
⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) |
129 |
128
|
ishaus |
⊢ ( ( 𝑅 ×t 𝑆 ) ∈ Haus ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∀ 𝑦 ∈ ∪ ( 𝑅 ×t 𝑆 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) ) |
130 |
4 127 129
|
sylanbrc |
⊢ ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑅 ×t 𝑆 ) ∈ Haus ) |