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

Theorem txbas 22170
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 5546 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥 × 𝑦) = (𝑎 × 𝑦))
3 xpeq2 5553 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑎 × 𝑦) = (𝑎 × 𝑏))
42, 3cbvmpov 7233 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑎𝑅, 𝑏𝑆 ↦ (𝑎 × 𝑏))
54rnmpo 7268 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
61, 5eqtri 2845 . . . . . . 7 𝐵 = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
76abeq2i 2949 . . . . . 6 (𝑢𝐵 ↔ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏))
8 xpeq1 5546 . . . . . . . . . 10 (𝑥 = 𝑐 → (𝑥 × 𝑦) = (𝑐 × 𝑦))
9 xpeq2 5553 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑐 × 𝑦) = (𝑐 × 𝑑))
108, 9cbvmpov 7233 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑐𝑅, 𝑑𝑆 ↦ (𝑐 × 𝑑))
1110rnmpo 7268 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
121, 11eqtri 2845 . . . . . . 7 𝐵 = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
1312abeq2i 2949 . . . . . 6 (𝑣𝐵 ↔ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑))
147, 13anbi12i 629 . . . . 5 ((𝑢𝐵𝑣𝐵) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
15 reeanv 3348 . . . . 5 (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
1614, 15bitr4i 281 . . . 4 ((𝑢𝐵𝑣𝐵) ↔ ∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
17 reeanv 3348 . . . . . 6 (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
18 basis2 21554 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ TopBases ∧ 𝑎𝑅) ∧ (𝑐𝑅𝑢 ∈ (𝑎𝑐))) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
1918exp43 440 . . . . . . . . . . . . . . 15 (𝑅 ∈ TopBases → (𝑎𝑅 → (𝑐𝑅 → (𝑢 ∈ (𝑎𝑐) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐))))))
2019imp42 430 . . . . . . . . . . . . . 14 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
21 basis2 21554 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ TopBases ∧ 𝑏𝑆) ∧ (𝑑𝑆𝑣 ∈ (𝑏𝑑))) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
2221exp43 440 . . . . . . . . . . . . . . 15 (𝑆 ∈ TopBases → (𝑏𝑆 → (𝑑𝑆 → (𝑣 ∈ (𝑏𝑑) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))))
2322imp42 430 . . . . . . . . . . . . . 14 (((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑)) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
24 reeanv 3348 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) ↔ (∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))
25 opelxpi 5569 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑥𝑣𝑦) → ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦))
26 xpss12 5547 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑)) → (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))
2725, 26anim12i 615 . . . . . . . . . . . . . . . . . 18 (((𝑢𝑥𝑣𝑦) ∧ (𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2827an4s 659 . . . . . . . . . . . . . . . . 17 (((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2928reximi 3231 . . . . . . . . . . . . . . . 16 (∃𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3029reximi 3231 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3124, 30sylbir 238 . . . . . . . . . . . . . 14 ((∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3220, 23, 31syl2an 598 . . . . . . . . . . . . 13 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) ∧ ((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3332an4s 659 . . . . . . . . . . . 12 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) ∧ (𝑢 ∈ (𝑎𝑐) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3433ralrimivva 3181 . . . . . . . . . . 11 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
35 eleq1 2901 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑢, 𝑣⟩ → (𝑝 ∈ (𝑥 × 𝑦) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦)))
3635anbi1d 632 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑢, 𝑣⟩ → ((𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
37362rexbidv 3286 . . . . . . . . . . . 12 (𝑝 = ⟨𝑢, 𝑣⟩ → (∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
3837ralxp 5689 . . . . . . . . . . 11 (∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3934, 38sylibr 237 . . . . . . . . . 10 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4039an4s 659 . . . . . . . . 9 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ ((𝑎𝑅𝑐𝑅) ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4140anassrs 471 . . . . . . . 8 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
42 ineq12 4158 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)))
43 inxp 5680 . . . . . . . . . 10 ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)) = ((𝑎𝑐) × (𝑏𝑑))
4442, 43syl6eq 2873 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎𝑐) × (𝑏𝑑)))
4544sseq2d 3974 . . . . . . . . . . . 12 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑡 ⊆ (𝑢𝑣) ↔ 𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4645anbi2d 631 . . . . . . . . . . 11 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ((𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
4746rexbidv 3283 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
481rexeqi 3391 . . . . . . . . . . 11 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
49 fvex 6665 . . . . . . . . . . . . . 14 (1st𝑧) ∈ V
50 fvex 6665 . . . . . . . . . . . . . 14 (2nd𝑧) ∈ V
5149, 50xpex 7461 . . . . . . . . . . . . 13 ((1st𝑧) × (2nd𝑧)) ∈ V
5251rgenw 3142 . . . . . . . . . . . 12 𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V
53 vex 3472 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
54 vex 3472 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
5553, 54op1std 7685 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5653, 54op2ndd 7686 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
5755, 56xpeq12d 5563 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) × (2nd𝑧)) = (𝑥 × 𝑦))
5857mpompt 7250 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧))) = (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))
5958eqcomi 2831 . . . . . . . . . . . . 13 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧)))
60 eleq2 2902 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑝𝑡𝑝 ∈ ((1st𝑧) × (2nd𝑧))))
61 sseq1 3967 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6260, 61anbi12d 633 . . . . . . . . . . . . 13 (𝑡 = ((1st𝑧) × (2nd𝑧)) → ((𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6359, 62rexrnmptw 6843 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V → (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6452, 63ax-mp 5 . . . . . . . . . . 11 (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6557eleq2d 2899 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ↔ 𝑝 ∈ (𝑥 × 𝑦)))
6657sseq1d 3973 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6765, 66anbi12d 633 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6867rexxp 5690 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6948, 64, 683bitri 300 . . . . . . . . . 10 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
7047, 69syl6bb 290 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7144, 70raleqbidv 3382 . . . . . . . 8 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7241, 71syl5ibrcom 250 . . . . . . 7 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7372rexlimdvva 3280 . . . . . 6 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7417, 73syl5bir 246 . . . . 5 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → ((∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7574rexlimdvva 3280 . . . 4 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7616, 75syl5bi 245 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ((𝑢𝐵𝑣𝐵) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7776ralrimivv 3180 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)))
781txbasex 22169 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ V)
79 isbasis2g 21551 . . 3 (𝐵 ∈ V → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8078, 79syl 17 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8177, 80mpbird 260 1 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2114  {cab 2800  wral 3130  wrex 3131  Vcvv 3469  cin 3907  wss 3908  cop 4545  cmpt 5122   × cxp 5530  ran crn 5533  cfv 6334  cmpo 7142  1st c1st 7673  2nd c2nd 7674  TopBasesctb 21548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-fv 6342  df-oprab 7144  df-mpo 7145  df-1st 7675  df-2nd 7676  df-bases 21549
This theorem is referenced by:  txtop  22172  tx2ndc  22254  mbfimaopnlem  24257
  Copyright terms: Public domain W3C validator