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

Theorem txbas 21418
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 5157 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥 × 𝑦) = (𝑎 × 𝑦))
3 xpeq2 5163 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝑎 × 𝑦) = (𝑎 × 𝑏))
42, 3cbvmpt2v 6777 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑎𝑅, 𝑏𝑆 ↦ (𝑎 × 𝑏))
54rnmpt2 6812 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
61, 5eqtri 2673 . . . . . . 7 𝐵 = {𝑢 ∣ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏)}
76abeq2i 2764 . . . . . 6 (𝑢𝐵 ↔ ∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏))
8 xpeq1 5157 . . . . . . . . . 10 (𝑥 = 𝑐 → (𝑥 × 𝑦) = (𝑐 × 𝑦))
9 xpeq2 5163 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑐 × 𝑦) = (𝑐 × 𝑑))
108, 9cbvmpt2v 6777 . . . . . . . . 9 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑐𝑅, 𝑑𝑆 ↦ (𝑐 × 𝑑))
1110rnmpt2 6812 . . . . . . . 8 ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
121, 11eqtri 2673 . . . . . . 7 𝐵 = {𝑣 ∣ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)}
1312abeq2i 2764 . . . . . 6 (𝑣𝐵 ↔ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑))
147, 13anbi12i 733 . . . . 5 ((𝑢𝐵𝑣𝐵) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
15 reeanv 3136 . . . . 5 (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑎𝑅𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐𝑅𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
1614, 15bitr4i 267 . . . 4 ((𝑢𝐵𝑣𝐵) ↔ ∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
17 reeanv 3136 . . . . . 6 (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)))
18 basis2 20803 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ TopBases ∧ 𝑎𝑅) ∧ (𝑐𝑅𝑢 ∈ (𝑎𝑐))) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
1918exp43 639 . . . . . . . . . . . . . . 15 (𝑅 ∈ TopBases → (𝑎𝑅 → (𝑐𝑅 → (𝑢 ∈ (𝑎𝑐) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐))))))
2019imp42 619 . . . . . . . . . . . . . 14 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) → ∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)))
21 basis2 20803 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ TopBases ∧ 𝑏𝑆) ∧ (𝑑𝑆𝑣 ∈ (𝑏𝑑))) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
2221exp43 639 . . . . . . . . . . . . . . 15 (𝑆 ∈ TopBases → (𝑏𝑆 → (𝑑𝑆 → (𝑣 ∈ (𝑏𝑑) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))))
2322imp42 619 . . . . . . . . . . . . . 14 (((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑)) → ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑)))
24 reeanv 3136 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) ↔ (∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))))
25 opelxpi 5182 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑥𝑣𝑦) → ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦))
26 xpss12 5158 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑)) → (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))
2725, 26anim12i 589 . . . . . . . . . . . . . . . . . 18 (((𝑢𝑥𝑣𝑦) ∧ (𝑥 ⊆ (𝑎𝑐) ∧ 𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2827an4s 886 . . . . . . . . . . . . . . . . 17 (((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
2928reximi 3040 . . . . . . . . . . . . . . . 16 (∃𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3029reximi 3040 . . . . . . . . . . . . . . 15 (∃𝑥𝑅𝑦𝑆 ((𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3124, 30sylbir 225 . . . . . . . . . . . . . 14 ((∃𝑥𝑅 (𝑢𝑥𝑥 ⊆ (𝑎𝑐)) ∧ ∃𝑦𝑆 (𝑣𝑦𝑦 ⊆ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3220, 23, 31syl2an 493 . . . . . . . . . . . . 13 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ 𝑢 ∈ (𝑎𝑐)) ∧ ((𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆)) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3332an4s 886 . . . . . . . . . . . 12 ((((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) ∧ (𝑢 ∈ (𝑎𝑐) ∧ 𝑣 ∈ (𝑏𝑑))) → ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3433ralrimivva 3000 . . . . . . . . . . 11 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
35 eleq1 2718 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑢, 𝑣⟩ → (𝑝 ∈ (𝑥 × 𝑦) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦)))
3635anbi1d 741 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑢, 𝑣⟩ → ((𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
37362rexbidv 3086 . . . . . . . . . . . 12 (𝑝 = ⟨𝑢, 𝑣⟩ → (∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
3837ralxp 5296 . . . . . . . . . . 11 (∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∀𝑢 ∈ (𝑎𝑐)∀𝑣 ∈ (𝑏𝑑)∃𝑥𝑅𝑦𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
3934, 38sylibr 224 . . . . . . . . . 10 (((𝑅 ∈ TopBases ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4039an4s 886 . . . . . . . . 9 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ ((𝑎𝑅𝑐𝑅) ∧ (𝑏𝑆𝑑𝑆))) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4140anassrs 681 . . . . . . . 8 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
42 ineq12 3842 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)))
43 inxp 5287 . . . . . . . . . 10 ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)) = ((𝑎𝑐) × (𝑏𝑑))
4442, 43syl6eq 2701 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢𝑣) = ((𝑎𝑐) × (𝑏𝑑)))
4544sseq2d 3666 . . . . . . . . . . . 12 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑡 ⊆ (𝑢𝑣) ↔ 𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
4645anbi2d 740 . . . . . . . . . . 11 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ((𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
4746rexbidv 3081 . . . . . . . . . 10 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
481rexeqi 3173 . . . . . . . . . . 11 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))))
49 fvex 6239 . . . . . . . . . . . . . 14 (1st𝑧) ∈ V
50 fvex 6239 . . . . . . . . . . . . . 14 (2nd𝑧) ∈ V
5149, 50xpex 7004 . . . . . . . . . . . . 13 ((1st𝑧) × (2nd𝑧)) ∈ V
5251rgenw 2953 . . . . . . . . . . . 12 𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V
53 vex 3234 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
54 vex 3234 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
5553, 54op1std 7220 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5653, 54op2ndd 7221 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
5755, 56xpeq12d 5174 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) × (2nd𝑧)) = (𝑥 × 𝑦))
5857mpt2mpt 6794 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧))) = (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))
5958eqcomi 2660 . . . . . . . . . . . . 13 (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦)) = (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st𝑧) × (2nd𝑧)))
60 eleq2 2719 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑝𝑡𝑝 ∈ ((1st𝑧) × (2nd𝑧))))
61 sseq1 3659 . . . . . . . . . . . . . 14 (𝑡 = ((1st𝑧) × (2nd𝑧)) → (𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6260, 61anbi12d 747 . . . . . . . . . . . . 13 (𝑡 = ((1st𝑧) × (2nd𝑧)) → ((𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6359, 62rexrnmpt 6409 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝑅 × 𝑆)((1st𝑧) × (2nd𝑧)) ∈ V → (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6452, 63ax-mp 5 . . . . . . . . . . 11 (∃𝑡 ∈ ran (𝑥𝑅, 𝑦𝑆 ↦ (𝑥 × 𝑦))(𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6557eleq2d 2716 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ↔ 𝑝 ∈ (𝑥 × 𝑦)))
6657sseq1d 3665 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑)) ↔ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6765, 66anbi12d 747 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
6867rexxp 5297 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st𝑧) × (2nd𝑧)) ∧ ((1st𝑧) × (2nd𝑧)) ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
6948, 64, 683bitri 286 . . . . . . . . . 10 (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ ((𝑎𝑐) × (𝑏𝑑))) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑))))
7047, 69syl6bb 276 . . . . . . . . 9 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7144, 70raleqbidv 3182 . . . . . . . 8 ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)) ↔ ∀𝑝 ∈ ((𝑎𝑐) × (𝑏𝑑))∃𝑥𝑅𝑦𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎𝑐) × (𝑏𝑑)))))
7241, 71syl5ibrcom 237 . . . . . . 7 ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) ∧ (𝑏𝑆𝑑𝑆)) → ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7372rexlimdvva 3067 . . . . . 6 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → (∃𝑏𝑆𝑑𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7417, 73syl5bir 233 . . . . 5 (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎𝑅𝑐𝑅)) → ((∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7574rexlimdvva 3067 . . . 4 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (∃𝑎𝑅𝑐𝑅 (∃𝑏𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7616, 75syl5bi 232 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ((𝑢𝐵𝑣𝐵) → ∀𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣))))
7776ralrimivv 2999 . 2 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ∀𝑢𝐵𝑣𝐵𝑝 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑝𝑡𝑡 ⊆ (𝑢𝑣)))
781txbasex 21417 . . 3 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ V)
79 isbasis2g 20800 . . 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 383   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  Vcvv 3231  cin 3606  wss 3607  cop 4216  cmpt 4762   × cxp 5141  ran crn 5144  cfv 5926  cmpt2 6692  1st c1st 7208  2nd c2nd 7209  TopBasesctb 20797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-bases 20798
This theorem is referenced by:  txtop  21420  tx2ndc  21502  mbfimaopnlem  23467
  Copyright terms: Public domain W3C validator