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

Theorem txbas 21590
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 5264 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥 × 𝑦) = (𝑎 × 𝑦))
3 xpeq2 5270 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑎 × 𝑦) = (𝑎 × 𝑏))
42, 3cbvmpt2v 6885 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑎𝑅, 𝑏𝑆 ↦ (𝑎 × 𝑏))
54rnmpt2 6920 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
61, 5eqtri 2793 . . . . . . 7 𝐵 = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
76abeq2i 2884 . . . . . 6 (𝑢𝐵 ↔ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏))
8 xpeq1 5264 . . . . . . . . . 10 (𝑥 = 𝑐 → (𝑥 × 𝑦) = (𝑐 × 𝑦))
9 xpeq2 5270 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑐 × 𝑦) = (𝑐 × 𝑑))
108, 9cbvmpt2v 6885 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑐𝑅, 𝑑𝑆 ↦ (𝑐 × 𝑑))
1110rnmpt2 6920 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
121, 11eqtri 2793 . . . . . . 7 𝐵 = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
1312abeq2i 2884 . . . . . 6 (𝑣𝐵 ↔ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑))
147, 13anbi12i 612 . . . . 5 ((𝑢𝐵𝑣𝐵) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
15 reeanv 3255 . . . . 5 (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
1614, 15bitr4i 267 . . . 4 ((𝑢𝐵𝑣𝐵) ↔ ∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
17 reeanv 3255 . . . . . 6 (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
18 basis2 20975 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ TopBases ∧ 𝑎𝑅) ∧ (𝑐𝑅𝑢 ∈ (𝑎𝑐))) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
1918exp43 423 . . . . . . . . . . . . . . 15 (𝑅 ∈ TopBases → (𝑎𝑅 → (𝑐𝑅 → (𝑢 ∈ (𝑎𝑐) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐))))))
2019imp42 413 . . . . . . . . . . . . . 14 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
21 basis2 20975 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ TopBases ∧ 𝑏𝑆) ∧ (𝑑𝑆𝑣 ∈ (𝑏𝑑))) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
2221exp43 423 . . . . . . . . . . . . . . 15 (𝑆 ∈ TopBases → (𝑏𝑆 → (𝑑𝑆 → (𝑣 ∈ (𝑏𝑑) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))))
2322imp42 413 . . . . . . . . . . . . . 14 (((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑)) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
24 reeanv 3255 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) ↔ (∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))
25 opelxpi 5287 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑥𝑣𝑦) → ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦))
26 xpss12 5265 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑)) → (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))
2725, 26anim12i 600 . . . . . . . . . . . . . . . . . 18 (((𝑢𝑥𝑣𝑦) ∧ (𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2827an4s 639 . . . . . . . . . . . . . . . . 17 (((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2928reximi 3159 . . . . . . . . . . . . . . . 16 (∃𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3029reximi 3159 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3124, 30sylbir 225 . . . . . . . . . . . . . 14 ((∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3220, 23, 31syl2an 583 . . . . . . . . . . . . 13 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) ∧ ((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3332an4s 639 . . . . . . . . . . . 12 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) ∧ (𝑢 ∈ (𝑎𝑐) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3433ralrimivva 3120 . . . . . . . . . . 11 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
35 eleq1 2838 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑢, 𝑣⟩ → (𝑝 ∈ (𝑥 × 𝑦) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦)))
3635anbi1d 615 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑢, 𝑣⟩ → ((𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
37362rexbidv 3205 . . . . . . . . . . . 12 (𝑝 = ⟨𝑢, 𝑣⟩ → (∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
3837ralxp 5401 . . . . . . . . . . 11 (∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3934, 38sylibr 224 . . . . . . . . . 10 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4039an4s 639 . . . . . . . . 9 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ ((𝑎𝑅𝑐𝑅) ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4140anassrs 453 . . . . . . . 8 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
42 ineq12 3960 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)))
43 inxp 5392 . . . . . . . . . 10 ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)) = ((𝑎𝑐) × (𝑏𝑑))
4442, 43syl6eq 2821 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎𝑐) × (𝑏𝑑)))
4544sseq2d 3782 . . . . . . . . . . . 12 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑡 ⊆ (𝑢𝑣) ↔ 𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4645anbi2d 614 . . . . . . . . . . 11 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ((𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
4746rexbidv 3200 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
481rexeqi 3292 . . . . . . . . . . 11 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
49 fvex 6344 . . . . . . . . . . . . . 14 (1st𝑧) ∈ V
50 fvex 6344 . . . . . . . . . . . . . 14 (2nd𝑧) ∈ V
5149, 50xpex 7112 . . . . . . . . . . . . 13 ((1st𝑧) × (2nd𝑧)) ∈ V
5251rgenw 3073 . . . . . . . . . . . 12 𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V
53 vex 3354 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
54 vex 3354 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
5553, 54op1std 7328 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5653, 54op2ndd 7329 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
5755, 56xpeq12d 5280 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) × (2nd𝑧)) = (𝑥 × 𝑦))
5857mpt2mpt 6902 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧))) = (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))
5958eqcomi 2780 . . . . . . . . . . . . 13 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧)))
60 eleq2 2839 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑝𝑡𝑝 ∈ ((1st𝑧) × (2nd𝑧))))
61 sseq1 3775 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6260, 61anbi12d 616 . . . . . . . . . . . . 13 (𝑡 = ((1st𝑧) × (2nd𝑧)) → ((𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6359, 62rexrnmpt 6514 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V → (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6452, 63ax-mp 5 . . . . . . . . . . 11 (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6557eleq2d 2836 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ↔ 𝑝 ∈ (𝑥 × 𝑦)))
6657sseq1d 3781 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6765, 66anbi12d 616 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6867rexxp 5402 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6948, 64, 683bitri 286 . . . . . . . . . 10 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
7047, 69syl6bb 276 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7144, 70raleqbidv 3301 . . . . . . . 8 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7241, 71syl5ibrcom 237 . . . . . . 7 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7372rexlimdvva 3186 . . . . . 6 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7417, 73syl5bir 233 . . . . 5 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → ((∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7574rexlimdvva 3186 . . . 4 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7616, 75syl5bi 232 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ((𝑢𝐵𝑣𝐵) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7776ralrimivv 3119 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)))
781txbasex 21589 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ V)
79 isbasis2g 20972 . . 3 (𝐵 ∈ V → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8078, 79syl 17 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (𝐵 ∈ TopBases ↔ ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
8177, 80mpbird 247 1 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  {cab 2757  wral 3061  wrex 3062  Vcvv 3351  cin 3722  wss 3723  cop 4323  cmpt 4864   × cxp 5248  ran crn 5251  cfv 6030  cmpt2 6797  1st c1st 7316  2nd c2nd 7317  TopBasesctb 20969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-fv 6038  df-oprab 6799  df-mpt2 6800  df-1st 7318  df-2nd 7319  df-bases 20970
This theorem is referenced by:  txtop  21592  tx2ndc  21674  mbfimaopnlem  23641
  Copyright terms: Public domain W3C validator