Step | Hyp | Ref
| Expression |
1 | | f2ndres 7082 |
. . 3
⊢
(2nd ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑌 |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑌) |
3 | | toponss 20544 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (TopOn‘𝑌) ∧ 𝑤 ∈ 𝑆) → 𝑤 ⊆ 𝑌) |
4 | 3 | adantll 746 |
. . . . . . . . 9
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → 𝑤 ⊆ 𝑌) |
5 | | xpss2 5152 |
. . . . . . . . 9
⊢ (𝑤 ⊆ 𝑌 → (𝑋 × 𝑤) ⊆ (𝑋 × 𝑌)) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → (𝑋 × 𝑤) ⊆ (𝑋 × 𝑌)) |
7 | 6 | sseld 3567 |
. . . . . . 7
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ (𝑋 × 𝑤) → 𝑧 ∈ (𝑋 × 𝑌))) |
8 | 7 | pm4.71rd 665 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ (𝑋 × 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑋 × 𝑤)))) |
9 | | ffn 5958 |
. . . . . . . 8
⊢
((2nd ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑌 → (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
10 | | elpreima 6245 |
. . . . . . . 8
⊢
((2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) → (𝑧 ∈ (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ ((2nd ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤))) |
11 | 1, 9, 10 | mp2b 10 |
. . . . . . 7
⊢ (𝑧 ∈ (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ ((2nd ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤)) |
12 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → ((2nd ↾ (𝑋 × 𝑌))‘𝑧) = (2nd ‘𝑧)) |
13 | 12 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (((2nd ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤 ↔ (2nd ‘𝑧) ∈ 𝑤)) |
14 | | 1st2nd2 7096 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
15 | | xp1st 7089 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (1st ‘𝑧) ∈ 𝑋) |
16 | | elxp6 7091 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑤) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑋 ∧ (2nd
‘𝑧) ∈ 𝑤))) |
17 | | anass 679 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑋) ∧
(2nd ‘𝑧)
∈ 𝑤) ↔ (𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
((1st ‘𝑧)
∈ 𝑋 ∧
(2nd ‘𝑧)
∈ 𝑤))) |
18 | 16, 17 | bitr4i 266 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋 × 𝑤) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (1st
‘𝑧) ∈ 𝑋) ∧ (2nd
‘𝑧) ∈ 𝑤)) |
19 | 18 | baib 942 |
. . . . . . . . . 10
⊢ ((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑋) → (𝑧 ∈ (𝑋 × 𝑤) ↔ (2nd ‘𝑧) ∈ 𝑤)) |
20 | 14, 15, 19 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (𝑧 ∈ (𝑋 × 𝑤) ↔ (2nd ‘𝑧) ∈ 𝑤)) |
21 | 13, 20 | bitr4d 270 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (((2nd ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤 ↔ 𝑧 ∈ (𝑋 × 𝑤))) |
22 | 21 | pm5.32i 667 |
. . . . . . 7
⊢ ((𝑧 ∈ (𝑋 × 𝑌) ∧ ((2nd ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑋 × 𝑤))) |
23 | 11, 22 | bitri 263 |
. . . . . 6
⊢ (𝑧 ∈ (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑋 × 𝑤))) |
24 | 8, 23 | syl6rbbr 278 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ 𝑧 ∈ (𝑋 × 𝑤))) |
25 | 24 | eqrdv 2608 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) = (𝑋 × 𝑤)) |
26 | | toponmax 20543 |
. . . . . 6
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝑅) |
27 | | txopn 21215 |
. . . . . . 7
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑤 ∈ 𝑆)) → (𝑋 × 𝑤) ∈ (𝑅 ×t 𝑆)) |
28 | 27 | expr 641 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑋 ∈ 𝑅) → (𝑤 ∈ 𝑆 → (𝑋 × 𝑤) ∈ (𝑅 ×t 𝑆))) |
29 | 26, 28 | mpidan 701 |
. . . . 5
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑤 ∈ 𝑆 → (𝑋 × 𝑤) ∈ (𝑅 ×t 𝑆))) |
30 | 29 | imp 444 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → (𝑋 × 𝑤) ∈ (𝑅 ×t 𝑆)) |
31 | 25, 30 | eqeltrd 2688 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑆) → (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)) |
32 | 31 | ralrimiva 2949 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ∀𝑤 ∈ 𝑆 (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)) |
33 | | txtopon 21204 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
34 | | iscn 20849 |
. . 3
⊢ (((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ((2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ↔ ((2nd ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑤 ∈ 𝑆 (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)))) |
35 | 33, 34 | sylancom 698 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ((2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ↔ ((2nd ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑤 ∈ 𝑆 (◡(2nd ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)))) |
36 | 2, 32, 35 | mpbir2and 959 |
1
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) |