| Step | Hyp | Ref
| Expression |
| 1 | | f1stres 8038 |
. . 3
⊢
(1st ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑋 |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑋) |
| 3 | | ffn 6736 |
. . . . . . . 8
⊢
((1st ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑋 → (1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
| 4 | | elpreima 7078 |
. . . . . . . 8
⊢
((1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) → (𝑧 ∈ (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ ((1st ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤))) |
| 5 | 1, 3, 4 | mp2b 10 |
. . . . . . 7
⊢ (𝑧 ∈ (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ ((1st ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤)) |
| 6 | | fvres 6925 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → ((1st ↾ (𝑋 × 𝑌))‘𝑧) = (1st ‘𝑧)) |
| 7 | 6 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (((1st ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤 ↔ (1st ‘𝑧) ∈ 𝑤)) |
| 8 | | 1st2nd2 8053 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 9 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (2nd ‘𝑧) ∈ 𝑌) |
| 10 | | elxp6 8048 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑤 × 𝑌) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑤 ∧ (2nd
‘𝑧) ∈ 𝑌))) |
| 11 | | anass 468 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑤) ∧
(2nd ‘𝑧)
∈ 𝑌) ↔ (𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
((1st ‘𝑧)
∈ 𝑤 ∧
(2nd ‘𝑧)
∈ 𝑌))) |
| 12 | | an32 646 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑤) ∧
(2nd ‘𝑧)
∈ 𝑌) ↔ ((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(2nd ‘𝑧)
∈ 𝑌) ∧
(1st ‘𝑧)
∈ 𝑤)) |
| 13 | 10, 11, 12 | 3bitr2i 299 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑤 × 𝑌) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (2nd
‘𝑧) ∈ 𝑌) ∧ (1st
‘𝑧) ∈ 𝑤)) |
| 14 | 13 | baib 535 |
. . . . . . . . . 10
⊢ ((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(2nd ‘𝑧)
∈ 𝑌) → (𝑧 ∈ (𝑤 × 𝑌) ↔ (1st ‘𝑧) ∈ 𝑤)) |
| 15 | 8, 9, 14 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (𝑧 ∈ (𝑤 × 𝑌) ↔ (1st ‘𝑧) ∈ 𝑤)) |
| 16 | 7, 15 | bitr4d 282 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (((1st ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤 ↔ 𝑧 ∈ (𝑤 × 𝑌))) |
| 17 | 16 | pm5.32i 574 |
. . . . . . 7
⊢ ((𝑧 ∈ (𝑋 × 𝑌) ∧ ((1st ↾ (𝑋 × 𝑌))‘𝑧) ∈ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑤 × 𝑌))) |
| 18 | 5, 17 | bitri 275 |
. . . . . 6
⊢ (𝑧 ∈ (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑤 × 𝑌))) |
| 19 | | toponss 22933 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝑅) → 𝑤 ⊆ 𝑋) |
| 20 | 19 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → 𝑤 ⊆ 𝑋) |
| 21 | | xpss1 5704 |
. . . . . . . . 9
⊢ (𝑤 ⊆ 𝑋 → (𝑤 × 𝑌) ⊆ (𝑋 × 𝑌)) |
| 22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → (𝑤 × 𝑌) ⊆ (𝑋 × 𝑌)) |
| 23 | 22 | sseld 3982 |
. . . . . . 7
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → (𝑧 ∈ (𝑤 × 𝑌) → 𝑧 ∈ (𝑋 × 𝑌))) |
| 24 | 23 | pm4.71rd 562 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → (𝑧 ∈ (𝑤 × 𝑌) ↔ (𝑧 ∈ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑤 × 𝑌)))) |
| 25 | 18, 24 | bitr4id 290 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → (𝑧 ∈ (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ↔ 𝑧 ∈ (𝑤 × 𝑌))) |
| 26 | 25 | eqrdv 2735 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) = (𝑤 × 𝑌)) |
| 27 | | toponmax 22932 |
. . . . . 6
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝑆) |
| 28 | 27 | ad2antlr 727 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → 𝑌 ∈ 𝑆) |
| 29 | | txopn 23610 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑤 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆)) → (𝑤 × 𝑌) ∈ (𝑅 ×t 𝑆)) |
| 30 | 29 | anassrs 467 |
. . . . 5
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) ∧ 𝑌 ∈ 𝑆) → (𝑤 × 𝑌) ∈ (𝑅 ×t 𝑆)) |
| 31 | 28, 30 | mpdan 687 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → (𝑤 × 𝑌) ∈ (𝑅 ×t 𝑆)) |
| 32 | 26, 31 | eqeltrd 2841 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑤 ∈ 𝑅) → (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)) |
| 33 | 32 | ralrimiva 3146 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ∀𝑤 ∈ 𝑅 (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)) |
| 34 | | txtopon 23599 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 35 | | simpl 482 |
. . 3
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑅 ∈ (TopOn‘𝑋)) |
| 36 | | iscn 23243 |
. . 3
⊢ (((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝑅 ∈ (TopOn‘𝑋)) → ((1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ↔ ((1st ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑋 ∧ ∀𝑤 ∈ 𝑅 (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)))) |
| 37 | 34, 35, 36 | syl2anc 584 |
. 2
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ((1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ↔ ((1st ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑋 ∧ ∀𝑤 ∈ 𝑅 (◡(1st ↾ (𝑋 × 𝑌)) “ 𝑤) ∈ (𝑅 ×t 𝑆)))) |
| 38 | 2, 33, 37 | mpbir2and 713 |
1
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) |