Step |
Hyp |
Ref |
Expression |
1 |
|
txcmpb.1 |
⊢ 𝑋 = ∪ 𝑅 |
2 |
|
txcmpb.2 |
⊢ 𝑌 = ∪ 𝑆 |
3 |
|
simpr |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 𝑅 ×t 𝑆 ) ∈ Comp ) |
4 |
|
simplrr |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑌 ≠ ∅ ) |
5 |
|
fo1stres |
⊢ ( 𝑌 ≠ ∅ → ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 ) |
6 |
4 5
|
syl |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 ) |
7 |
1 2
|
txuni |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
8 |
7
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
9 |
|
foeq2 |
⊢ ( ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 ↔ ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 ) ) |
10 |
8 9
|
syl |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 ↔ ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 ) ) |
11 |
6 10
|
mpbid |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 ) |
12 |
1
|
toptopon |
⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) |
13 |
2
|
toptopon |
⊢ ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) |
14 |
|
tx1cn |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) |
15 |
12 13 14
|
syl2anb |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) |
16 |
15
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) |
17 |
1
|
cncmp |
⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Comp ∧ ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 ∧ ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) → 𝑅 ∈ Comp ) |
18 |
3 11 16 17
|
syl3anc |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑅 ∈ Comp ) |
19 |
|
simplrl |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑋 ≠ ∅ ) |
20 |
|
fo2ndres |
⊢ ( 𝑋 ≠ ∅ → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 ) |
21 |
19 20
|
syl |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 ) |
22 |
|
foeq2 |
⊢ ( ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 ↔ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 ) ) |
23 |
8 22
|
syl |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 ↔ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 ) ) |
24 |
21 23
|
mpbid |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 ) |
25 |
|
tx2cn |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) |
26 |
12 13 25
|
syl2anb |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) |
27 |
26
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) |
28 |
2
|
cncmp |
⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Comp ∧ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 ∧ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) → 𝑆 ∈ Comp ) |
29 |
3 24 27 28
|
syl3anc |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑆 ∈ Comp ) |
30 |
18 29
|
jca |
⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ) |
31 |
30
|
ex |
⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑅 ×t 𝑆 ) ∈ Comp → ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ) ) |
32 |
|
txcmp |
⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ( 𝑅 ×t 𝑆 ) ∈ Comp ) |
33 |
31 32
|
impbid1 |
⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑅 ×t 𝑆 ) ∈ Comp ↔ ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ) ) |