MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txbas Structured version   Visualization version   GIF version

Theorem txbas 21879
Description: The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
txval.1 𝐵 = ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))
Assertion
Ref Expression
txbas ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases)
Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝑆,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)

Proof of Theorem txbas
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑝 𝑡 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txval.1 . . . . . . . 8 𝐵 = ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))
2 xpeq1 5421 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥 × 𝑦) = (𝑎 × 𝑦))
3 xpeq2 5428 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑎 × 𝑦) = (𝑎 × 𝑏))
42, 3cbvmpov 7065 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑎𝑅, 𝑏𝑆 ↦ (𝑎 × 𝑏))
54rnmpo 7100 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
61, 5eqtri 2802 . . . . . . 7 𝐵 = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
76abeq2i 2900 . . . . . 6 (𝑢𝐵 ↔ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏))
8 xpeq1 5421 . . . . . . . . . 10 (𝑥 = 𝑐 → (𝑥 × 𝑦) = (𝑐 × 𝑦))
9 xpeq2 5428 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑐 × 𝑦) = (𝑐 × 𝑑))
108, 9cbvmpov 7065 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑐𝑅, 𝑑𝑆 ↦ (𝑐 × 𝑑))
1110rnmpo 7100 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
121, 11eqtri 2802 . . . . . . 7 𝐵 = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
1312abeq2i 2900 . . . . . 6 (𝑣𝐵 ↔ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑))
147, 13anbi12i 617 . . . . 5 ((𝑢𝐵𝑣𝐵) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
15 reeanv 3308 . . . . 5 (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
1614, 15bitr4i 270 . . . 4 ((𝑢𝐵𝑣𝐵) ↔ ∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
17 reeanv 3308 . . . . . 6 (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
18 basis2 21263 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ TopBases ∧ 𝑎𝑅) ∧ (𝑐𝑅𝑢 ∈ (𝑎𝑐))) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
1918exp43 429 . . . . . . . . . . . . . . 15 (𝑅 ∈ TopBases → (𝑎𝑅 → (𝑐𝑅 → (𝑢 ∈ (𝑎𝑐) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐))))))
2019imp42 419 . . . . . . . . . . . . . 14 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
21 basis2 21263 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ TopBases ∧ 𝑏𝑆) ∧ (𝑑𝑆𝑣 ∈ (𝑏𝑑))) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
2221exp43 429 . . . . . . . . . . . . . . 15 (𝑆 ∈ TopBases → (𝑏𝑆 → (𝑑𝑆 → (𝑣 ∈ (𝑏𝑑) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))))
2322imp42 419 . . . . . . . . . . . . . 14 (((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑)) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
24 reeanv 3308 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) ↔ (∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))
25 opelxpi 5444 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑥𝑣𝑦) → ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦))
26 xpss12 5422 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑)) → (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))
2725, 26anim12i 603 . . . . . . . . . . . . . . . . . 18 (((𝑢𝑥𝑣𝑦) ∧ (𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2827an4s 647 . . . . . . . . . . . . . . . . 17 (((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2928reximi 3190 . . . . . . . . . . . . . . . 16 (∃𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3029reximi 3190 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3124, 30sylbir 227 . . . . . . . . . . . . . 14 ((∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3220, 23, 31syl2an 586 . . . . . . . . . . . . 13 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) ∧ ((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3332an4s 647 . . . . . . . . . . . 12 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) ∧ (𝑢 ∈ (𝑎𝑐) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3433ralrimivva 3141 . . . . . . . . . . 11 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
35 eleq1 2853 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑢, 𝑣⟩ → (𝑝 ∈ (𝑥 × 𝑦) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦)))
3635anbi1d 620 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑢, 𝑣⟩ → ((𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
37362rexbidv 3245 . . . . . . . . . . . 12 (𝑝 = ⟨𝑢, 𝑣⟩ → (∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
3837ralxp 5562 . . . . . . . . . . 11 (∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3934, 38sylibr 226 . . . . . . . . . 10 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4039an4s 647 . . . . . . . . 9 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ ((𝑎𝑅𝑐𝑅) ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4140anassrs 460 . . . . . . . 8 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
42 ineq12 4071 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)))
43 inxp 5553 . . . . . . . . . 10 ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)) = ((𝑎𝑐) × (𝑏𝑑))
4442, 43syl6eq 2830 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎𝑐) × (𝑏𝑑)))
4544sseq2d 3889 . . . . . . . . . . . 12 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑡 ⊆ (𝑢𝑣) ↔ 𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4645anbi2d 619 . . . . . . . . . . 11 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ((𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
4746rexbidv 3242 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
481rexeqi 3354 . . . . . . . . . . 11 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
49 fvex 6512 . . . . . . . . . . . . . 14 (1st𝑧) ∈ V
50 fvex 6512 . . . . . . . . . . . . . 14 (2nd𝑧) ∈ V
5149, 50xpex 7293 . . . . . . . . . . . . 13 ((1st𝑧) × (2nd𝑧)) ∈ V
5251rgenw 3100 . . . . . . . . . . . 12 𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V
53 vex 3418 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
54 vex 3418 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
5553, 54op1std 7511 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5653, 54op2ndd 7512 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
5755, 56xpeq12d 5438 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) × (2nd𝑧)) = (𝑥 × 𝑦))
5857mpompt 7082 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧))) = (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))
5958eqcomi 2787 . . . . . . . . . . . . 13 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧)))
60 eleq2 2854 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑝𝑡𝑝 ∈ ((1st𝑧) × (2nd𝑧))))
61 sseq1 3882 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6260, 61anbi12d 621 . . . . . . . . . . . . 13 (𝑡 = ((1st𝑧) × (2nd𝑧)) → ((𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6359, 62rexrnmpt 6686 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V → (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6452, 63ax-mp 5 . . . . . . . . . . 11 (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6557eleq2d 2851 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ↔ 𝑝 ∈ (𝑥 × 𝑦)))
6657sseq1d 3888 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6765, 66anbi12d 621 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6867rexxp 5563 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6948, 64, 683bitri 289 . . . . . . . . . 10 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
7047, 69syl6bb 279 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7144, 70raleqbidv 3341 . . . . . . . 8 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7241, 71syl5ibrcom 239 . . . . . . 7 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7372rexlimdvva 3239 . . . . . 6 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7417, 73syl5bir 235 . . . . 5 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → ((∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7574rexlimdvva 3239 . . . 4 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7616, 75syl5bi 234 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ((𝑢𝐵𝑣𝐵) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7776ralrimivv 3140 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)))
781txbasex 21878 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ V)
79 isbasis2g 21260 . . 3 (𝐵 ∈ V → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8078, 79syl 17 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8177, 80mpbird 249 1 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  {cab 2758  wral 3088  wrex 3089  Vcvv 3415  cin 3828  wss 3829  cop 4447  cmpt 5008   × cxp 5405  ran crn 5408  cfv 6188  cmpo 6978  1st c1st 7499  2nd c2nd 7500  TopBasesctb 21257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-fv 6196  df-oprab 6980  df-mpo 6981  df-1st 7501  df-2nd 7502  df-bases 21258
This theorem is referenced by:  txtop  21881  tx2ndc  21963  mbfimaopnlem  23959
  Copyright terms: Public domain W3C validator