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

Theorem txbas 21592
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 5336 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥 × 𝑦) = (𝑎 × 𝑦))
3 xpeq2 5342 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑎 × 𝑦) = (𝑎 × 𝑏))
42, 3cbvmpt2v 6972 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑎𝑅, 𝑏𝑆 ↦ (𝑎 × 𝑏))
54rnmpt2 7007 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
61, 5eqtri 2839 . . . . . . 7 𝐵 = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
76abeq2i 2930 . . . . . 6 (𝑢𝐵 ↔ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏))
8 xpeq1 5336 . . . . . . . . . 10 (𝑥 = 𝑐 → (𝑥 × 𝑦) = (𝑐 × 𝑦))
9 xpeq2 5342 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑐 × 𝑦) = (𝑐 × 𝑑))
108, 9cbvmpt2v 6972 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑐𝑅, 𝑑𝑆 ↦ (𝑐 × 𝑑))
1110rnmpt2 7007 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
121, 11eqtri 2839 . . . . . . 7 𝐵 = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
1312abeq2i 2930 . . . . . 6 (𝑣𝐵 ↔ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑))
147, 13anbi12i 614 . . . . 5 ((𝑢𝐵𝑣𝐵) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
15 reeanv 3306 . . . . 5 (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
1614, 15bitr4i 269 . . . 4 ((𝑢𝐵𝑣𝐵) ↔ ∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
17 reeanv 3306 . . . . . 6 (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
18 basis2 20977 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ TopBases ∧ 𝑎𝑅) ∧ (𝑐𝑅𝑢 ∈ (𝑎𝑐))) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
1918exp43 425 . . . . . . . . . . . . . . 15 (𝑅 ∈ TopBases → (𝑎𝑅 → (𝑐𝑅 → (𝑢 ∈ (𝑎𝑐) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐))))))
2019imp42 415 . . . . . . . . . . . . . 14 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
21 basis2 20977 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ TopBases ∧ 𝑏𝑆) ∧ (𝑑𝑆𝑣 ∈ (𝑏𝑑))) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
2221exp43 425 . . . . . . . . . . . . . . 15 (𝑆 ∈ TopBases → (𝑏𝑆 → (𝑑𝑆 → (𝑣 ∈ (𝑏𝑑) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))))
2322imp42 415 . . . . . . . . . . . . . 14 (((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑)) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
24 reeanv 3306 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) ↔ (∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))
25 opelxpi 5359 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑥𝑣𝑦) → ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦))
26 xpss12 5337 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑)) → (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))
2725, 26anim12i 602 . . . . . . . . . . . . . . . . . 18 (((𝑢𝑥𝑣𝑦) ∧ (𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2827an4s 642 . . . . . . . . . . . . . . . . 17 (((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2928reximi 3209 . . . . . . . . . . . . . . . 16 (∃𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3029reximi 3209 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3124, 30sylbir 226 . . . . . . . . . . . . . 14 ((∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3220, 23, 31syl2an 585 . . . . . . . . . . . . 13 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) ∧ ((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3332an4s 642 . . . . . . . . . . . 12 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) ∧ (𝑢 ∈ (𝑎𝑐) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3433ralrimivva 3170 . . . . . . . . . . 11 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
35 eleq1 2884 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑢, 𝑣⟩ → (𝑝 ∈ (𝑥 × 𝑦) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦)))
3635anbi1d 617 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑢, 𝑣⟩ → ((𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
37362rexbidv 3256 . . . . . . . . . . . 12 (𝑝 = ⟨𝑢, 𝑣⟩ → (∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
3837ralxp 5476 . . . . . . . . . . 11 (∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3934, 38sylibr 225 . . . . . . . . . 10 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4039an4s 642 . . . . . . . . 9 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ ((𝑎𝑅𝑐𝑅) ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4140anassrs 455 . . . . . . . 8 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
42 ineq12 4019 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)))
43 inxp 5467 . . . . . . . . . 10 ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)) = ((𝑎𝑐) × (𝑏𝑑))
4442, 43syl6eq 2867 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎𝑐) × (𝑏𝑑)))
4544sseq2d 3841 . . . . . . . . . . . 12 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑡 ⊆ (𝑢𝑣) ↔ 𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4645anbi2d 616 . . . . . . . . . . 11 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ((𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
4746rexbidv 3251 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
481rexeqi 3343 . . . . . . . . . . 11 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
49 fvex 6428 . . . . . . . . . . . . . 14 (1st𝑧) ∈ V
50 fvex 6428 . . . . . . . . . . . . . 14 (2nd𝑧) ∈ V
5149, 50xpex 7199 . . . . . . . . . . . . 13 ((1st𝑧) × (2nd𝑧)) ∈ V
5251rgenw 3123 . . . . . . . . . . . 12 𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V
53 vex 3405 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
54 vex 3405 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
5553, 54op1std 7415 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5653, 54op2ndd 7416 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
5755, 56xpeq12d 5352 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) × (2nd𝑧)) = (𝑥 × 𝑦))
5857mpt2mpt 6989 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧))) = (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))
5958eqcomi 2826 . . . . . . . . . . . . 13 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧)))
60 eleq2 2885 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑝𝑡𝑝 ∈ ((1st𝑧) × (2nd𝑧))))
61 sseq1 3834 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6260, 61anbi12d 618 . . . . . . . . . . . . 13 (𝑡 = ((1st𝑧) × (2nd𝑧)) → ((𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6359, 62rexrnmpt 6598 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V → (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6452, 63ax-mp 5 . . . . . . . . . . 11 (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6557eleq2d 2882 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ↔ 𝑝 ∈ (𝑥 × 𝑦)))
6657sseq1d 3840 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6765, 66anbi12d 618 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6867rexxp 5477 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6948, 64, 683bitri 288 . . . . . . . . . 10 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
7047, 69syl6bb 278 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7144, 70raleqbidv 3352 . . . . . . . 8 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7241, 71syl5ibrcom 238 . . . . . . 7 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7372rexlimdvva 3237 . . . . . 6 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7417, 73syl5bir 234 . . . . 5 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → ((∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7574rexlimdvva 3237 . . . 4 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7616, 75syl5bi 233 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ((𝑢𝐵𝑣𝐵) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7776ralrimivv 3169 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)))
781txbasex 21591 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ V)
79 isbasis2g 20974 . . 3 (𝐵 ∈ V → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8078, 79syl 17 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8177, 80mpbird 248 1 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  {cab 2803  wral 3107  wrex 3108  Vcvv 3402  cin 3779  wss 3780  cop 4387  cmpt 4934   × cxp 5320  ran crn 5323  cfv 6108  cmpt2 6883  1st c1st 7403  2nd c2nd 7404  TopBasesctb 20971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5230  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-fv 6116  df-oprab 6885  df-mpt2 6886  df-1st 7405  df-2nd 7406  df-bases 20972
This theorem is referenced by:  txtop  21594  tx2ndc  21676  mbfimaopnlem  23646
  Copyright terms: Public domain W3C validator