| Step | Hyp | Ref
| Expression |
| 1 | | is2ndc 23454 |
. 2
⊢ (𝑅 ∈ 2ndω
↔ ∃𝑟 ∈
TopBases (𝑟 ≼ ω
∧ (topGen‘𝑟) =
𝑅)) |
| 2 | | is2ndc 23454 |
. 2
⊢ (𝑆 ∈ 2ndω
↔ ∃𝑠 ∈
TopBases (𝑠 ≼ ω
∧ (topGen‘𝑠) =
𝑆)) |
| 3 | | reeanv 3229 |
. . 3
⊢
(∃𝑟 ∈
TopBases ∃𝑠 ∈
TopBases ((𝑟 ≼
ω ∧ (topGen‘𝑟) = 𝑅) ∧ (𝑠 ≼ ω ∧ (topGen‘𝑠) = 𝑆)) ↔ (∃𝑟 ∈ TopBases (𝑟 ≼ ω ∧ (topGen‘𝑟) = 𝑅) ∧ ∃𝑠 ∈ TopBases (𝑠 ≼ ω ∧ (topGen‘𝑠) = 𝑆))) |
| 4 | | an4 656 |
. . . . 5
⊢ (((𝑟 ≼ ω ∧
(topGen‘𝑟) = 𝑅) ∧ (𝑠 ≼ ω ∧ (topGen‘𝑠) = 𝑆)) ↔ ((𝑟 ≼ ω ∧ 𝑠 ≼ ω) ∧ ((topGen‘𝑟) = 𝑅 ∧ (topGen‘𝑠) = 𝑆))) |
| 5 | | txbasval 23614 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) →
((topGen‘𝑟)
×t (topGen‘𝑠)) = (𝑟 ×t 𝑠)) |
| 6 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) = ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) |
| 7 | 6 | txval 23572 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) → (𝑟 ×t 𝑠) = (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |
| 8 | 5, 7 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) →
((topGen‘𝑟)
×t (topGen‘𝑠)) = (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) →
((topGen‘𝑟)
×t (topGen‘𝑠)) = (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |
| 10 | 6 | txbas 23575 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) → ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ∈ TopBases) |
| 11 | 10 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ∈ TopBases) |
| 12 | | omelon 9686 |
. . . . . . . . . . . 12
⊢ ω
∈ On |
| 13 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V |
| 14 | 13 | xpdom1 9111 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ≼ ω → (𝑟 × 𝑠) ≼ (ω × 𝑠)) |
| 15 | | omex 9683 |
. . . . . . . . . . . . . . . 16
⊢ ω
∈ V |
| 16 | 15 | xpdom2 9107 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ≼ ω → (ω
× 𝑠) ≼ (ω
× ω)) |
| 17 | | domtr 9047 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 × 𝑠) ≼ (ω × 𝑠) ∧ (ω × 𝑠) ≼ (ω × ω)) →
(𝑟 × 𝑠) ≼ (ω ×
ω)) |
| 18 | 14, 16, 17 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ≼ ω ∧ 𝑠 ≼ ω) → (𝑟 × 𝑠) ≼ (ω ×
ω)) |
| 19 | 18 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → (𝑟 × 𝑠) ≼ (ω ×
ω)) |
| 20 | | xpomen 10055 |
. . . . . . . . . . . . 13
⊢ (ω
× ω) ≈ ω |
| 21 | | domentr 9053 |
. . . . . . . . . . . . 13
⊢ (((𝑟 × 𝑠) ≼ (ω × ω) ∧
(ω × ω) ≈ ω) → (𝑟 × 𝑠) ≼ ω) |
| 22 | 19, 20, 21 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → (𝑟 × 𝑠) ≼ ω) |
| 23 | | ondomen 10077 |
. . . . . . . . . . . 12
⊢ ((ω
∈ On ∧ (𝑟 ×
𝑠) ≼ ω) →
(𝑟 × 𝑠) ∈ dom
card) |
| 24 | 12, 22, 23 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → (𝑟 × 𝑠) ∈ dom card) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) = (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) |
| 26 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
| 27 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
| 28 | 26, 27 | xpex 7773 |
. . . . . . . . . . . . . 14
⊢ (𝑥 × 𝑦) ∈ V |
| 29 | 25, 28 | fnmpoi 8095 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) Fn (𝑟 × 𝑠) |
| 30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) Fn (𝑟 × 𝑠)) |
| 31 | | dffn4 6826 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) Fn (𝑟 × 𝑠) ↔ (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)):(𝑟 × 𝑠)–onto→ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))) |
| 32 | 30, 31 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)):(𝑟 × 𝑠)–onto→ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))) |
| 33 | | fodomnum 10097 |
. . . . . . . . . . 11
⊢ ((𝑟 × 𝑠) ∈ dom card → ((𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)):(𝑟 × 𝑠)–onto→ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) → ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ≼ (𝑟 × 𝑠))) |
| 34 | 24, 32, 33 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ≼ (𝑟 × 𝑠)) |
| 35 | | domtr 9047 |
. . . . . . . . . 10
⊢ ((ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ≼ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ≼ ω) → ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ≼ ω) |
| 36 | 34, 22, 35 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) → ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ≼ ω) |
| 37 | | 2ndci 23456 |
. . . . . . . . 9
⊢ ((ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ∈ TopBases ∧ ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))) ∈
2ndω) |
| 38 | 11, 36, 37 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) →
(topGen‘ran (𝑥 ∈
𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))) ∈
2ndω) |
| 39 | 9, 38 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) →
((topGen‘𝑟)
×t (topGen‘𝑠)) ∈
2ndω) |
| 40 | | oveq12 7440 |
. . . . . . . 8
⊢
(((topGen‘𝑟) =
𝑅 ∧ (topGen‘𝑠) = 𝑆) → ((topGen‘𝑟) ×t (topGen‘𝑠)) = (𝑅 ×t 𝑆)) |
| 41 | 40 | eleq1d 2826 |
. . . . . . 7
⊢
(((topGen‘𝑟) =
𝑅 ∧ (topGen‘𝑠) = 𝑆) → (((topGen‘𝑟) ×t (topGen‘𝑠)) ∈ 2ndω
↔ (𝑅
×t 𝑆)
∈ 2ndω)) |
| 42 | 39, 41 | syl5ibcom 245 |
. . . . . 6
⊢ (((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) ∧ (𝑟 ≼ ω ∧ 𝑠 ≼ ω)) →
(((topGen‘𝑟) = 𝑅 ∧ (topGen‘𝑠) = 𝑆) → (𝑅 ×t 𝑆) ∈
2ndω)) |
| 43 | 42 | expimpd 453 |
. . . . 5
⊢ ((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) →
(((𝑟 ≼ ω ∧
𝑠 ≼ ω) ∧
((topGen‘𝑟) = 𝑅 ∧ (topGen‘𝑠) = 𝑆)) → (𝑅 ×t 𝑆) ∈
2ndω)) |
| 44 | 4, 43 | biimtrid 242 |
. . . 4
⊢ ((𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases) →
(((𝑟 ≼ ω ∧
(topGen‘𝑟) = 𝑅) ∧ (𝑠 ≼ ω ∧ (topGen‘𝑠) = 𝑆)) → (𝑅 ×t 𝑆) ∈
2ndω)) |
| 45 | 44 | rexlimivv 3201 |
. . 3
⊢
(∃𝑟 ∈
TopBases ∃𝑠 ∈
TopBases ((𝑟 ≼
ω ∧ (topGen‘𝑟) = 𝑅) ∧ (𝑠 ≼ ω ∧ (topGen‘𝑠) = 𝑆)) → (𝑅 ×t 𝑆) ∈
2ndω) |
| 46 | 3, 45 | sylbir 235 |
. 2
⊢
((∃𝑟 ∈
TopBases (𝑟 ≼ ω
∧ (topGen‘𝑟) =
𝑅) ∧ ∃𝑠 ∈ TopBases (𝑠 ≼ ω ∧
(topGen‘𝑠) = 𝑆)) → (𝑅 ×t 𝑆) ∈
2ndω) |
| 47 | 1, 2, 46 | syl2anb 598 |
1
⊢ ((𝑅 ∈ 2ndω
∧ 𝑆 ∈
2ndω) → (𝑅 ×t 𝑆) ∈
2ndω) |