txbas

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)

		Ref	Expression
	Hypothesis	txval.1	⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
	Assertion	txbas	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → 𝐵 ∈ TopBases )

Proof

Step	Hyp	Ref	Expression
1		txval.1	⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
2		xpeq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 × 𝑦 ) = ( 𝑎 × 𝑦 ) )
3		xpeq2	⊢ ( 𝑦 = 𝑏 → ( 𝑎 × 𝑦 ) = ( 𝑎 × 𝑏 ) )
4	2 3	cbvmpov	⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑆 ↦ ( 𝑎 × 𝑏 ) )
5	4	rnmpo	⊢ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = { 𝑢 ∣ ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) }
6	1 5	eqtri	⊢ 𝐵 = { 𝑢 ∣ ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) }
7	6	abeq2i	⊢ ( 𝑢 ∈ 𝐵 ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) )
8		xpeq1	⊢ ( 𝑥 = 𝑐 → ( 𝑥 × 𝑦 ) = ( 𝑐 × 𝑦 ) )
9		xpeq2	⊢ ( 𝑦 = 𝑑 → ( 𝑐 × 𝑦 ) = ( 𝑐 × 𝑑 ) )
10	8 9	cbvmpov	⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑐 ∈ 𝑅 , 𝑑 ∈ 𝑆 ↦ ( 𝑐 × 𝑑 ) )
11	10	rnmpo	⊢ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = { 𝑣 ∣ ∃ 𝑐 ∈ 𝑅 ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) }
12	1 11	eqtri	⊢ 𝐵 = { 𝑣 ∣ ∃ 𝑐 ∈ 𝑅 ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) }
13	12	abeq2i	⊢ ( 𝑣 ∈ 𝐵 ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) )
14	7 13	anbi12i	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ↔ ( ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) ∧ ∃ 𝑐 ∈ 𝑅 ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) ) )
15		reeanv	⊢ ( ∃ 𝑎 ∈ 𝑅 ∃ 𝑐 ∈ 𝑅 ( ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) ∧ ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) ) ↔ ( ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) ∧ ∃ 𝑐 ∈ 𝑅 ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) ) )
16	14 15	bitr4i	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑐 ∈ 𝑅 ( ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) ∧ ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) ) )
17		reeanv	⊢ ( ∃ 𝑏 ∈ 𝑆 ∃ 𝑑 ∈ 𝑆 ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) ↔ ( ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) ∧ ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) ) )
18		basis2	⊢ ( ( ( 𝑅 ∈ TopBases ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑢 ∈ ( 𝑎 ∩ 𝑐 ) ) ) → ∃ 𝑥 ∈ 𝑅 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) )
19	18	exp43	⊢ ( 𝑅 ∈ TopBases → ( 𝑎 ∈ 𝑅 → ( 𝑐 ∈ 𝑅 → ( 𝑢 ∈ ( 𝑎 ∩ 𝑐 ) → ∃ 𝑥 ∈ 𝑅 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) ) ) ) )
20	19	imp42	⊢ ( ( ( 𝑅 ∈ TopBases ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) ∧ 𝑢 ∈ ( 𝑎 ∩ 𝑐 ) ) → ∃ 𝑥 ∈ 𝑅 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) )
21		basis2	⊢ ( ( ( 𝑆 ∈ TopBases ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑑 ∈ 𝑆 ∧ 𝑣 ∈ ( 𝑏 ∩ 𝑑 ) ) ) → ∃ 𝑦 ∈ 𝑆 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) )
22	21	exp43	⊢ ( 𝑆 ∈ TopBases → ( 𝑏 ∈ 𝑆 → ( 𝑑 ∈ 𝑆 → ( 𝑣 ∈ ( 𝑏 ∩ 𝑑 ) → ∃ 𝑦 ∈ 𝑆 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) ) ) )
23	22	imp42	⊢ ( ( ( 𝑆 ∈ TopBases ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ∧ 𝑣 ∈ ( 𝑏 ∩ 𝑑 ) ) → ∃ 𝑦 ∈ 𝑆 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) )
24		reeanv	⊢ ( ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) ∧ ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝑅 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) ∧ ∃ 𝑦 ∈ 𝑆 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) )
25		opelxpi	⊢ ( ( 𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦 ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) )
26		xpss12	⊢ ( ( 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) → ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) )
27	25 26	anim12i	⊢ ( ( ( 𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦 ) ∧ ( 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
28	27	an4s	⊢ ( ( ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) ∧ ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
29	28	reximi	⊢ ( ∃ 𝑦 ∈ 𝑆 ( ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) ∧ ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) → ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
30	29	reximi	⊢ ( ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) ∧ ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
31	24 30	sylbir	⊢ ( ( ∃ 𝑥 ∈ 𝑅 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑎 ∩ 𝑐 ) ) ∧ ∃ 𝑦 ∈ 𝑆 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝑏 ∩ 𝑑 ) ) ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
32	20 23 31	syl2an	⊢ ( ( ( ( 𝑅 ∈ TopBases ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) ∧ 𝑢 ∈ ( 𝑎 ∩ 𝑐 ) ) ∧ ( ( 𝑆 ∈ TopBases ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ∧ 𝑣 ∈ ( 𝑏 ∩ 𝑑 ) ) ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
33	32	an4s	⊢ ( ( ( ( 𝑅 ∈ TopBases ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) ∧ ( 𝑆 ∈ TopBases ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) ∧ ( 𝑢 ∈ ( 𝑎 ∩ 𝑐 ) ∧ 𝑣 ∈ ( 𝑏 ∩ 𝑑 ) ) ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
34	33	ralrimivva	⊢ ( ( ( 𝑅 ∈ TopBases ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) ∧ ( 𝑆 ∈ TopBases ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ∀ 𝑢 ∈ ( 𝑎 ∩ 𝑐 ) ∀ 𝑣 ∈ ( 𝑏 ∩ 𝑑 ) ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
35		eleq1	⊢ ( 𝑝 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ) )
36	35	anbi1d	⊢ ( 𝑝 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
37	36	2rexbidv	⊢ ( 𝑝 = ⟨ 𝑢 , 𝑣 ⟩ → ( ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
38	37	ralxp	⊢ ( ∀ 𝑝 ∈ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ∀ 𝑢 ∈ ( 𝑎 ∩ 𝑐 ) ∀ 𝑣 ∈ ( 𝑏 ∩ 𝑑 ) ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
39	34 38	sylibr	⊢ ( ( ( 𝑅 ∈ TopBases ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) ∧ ( 𝑆 ∈ TopBases ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ∀ 𝑝 ∈ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
40	39	an4s	⊢ ( ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) ∧ ( ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ∀ 𝑝 ∈ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
41	40	anassrs	⊢ ( ( ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ∀ 𝑝 ∈ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
42		ineq12	⊢ ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ( 𝑢 ∩ 𝑣 ) = ( ( 𝑎 × 𝑏 ) ∩ ( 𝑐 × 𝑑 ) ) )
43		inxp	⊢ ( ( 𝑎 × 𝑏 ) ∩ ( 𝑐 × 𝑑 ) ) = ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) )
44	42 43	eqtrdi	⊢ ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ( 𝑢 ∩ 𝑣 ) = ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) )
45	44	sseq2d	⊢ ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ( 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ↔ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
46	45	anbi2d	⊢ ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ( ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ↔ ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
47	46	rexbidv	⊢ ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ( ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
48	1	rexeqi	⊢ ( ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
49		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
50		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
51	49 50	xpex	⊢ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∈ V
52	51	rgenw	⊢ ∀ 𝑧 ∈ ( 𝑅 × 𝑆 ) ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∈ V
53		vex	⊢ 𝑥 ∈ V
54		vex	⊢ 𝑦 ∈ V
55	53 54	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑥 )
56	53 54	op2ndd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑧 ) = 𝑦 )
57	55 56	xpeq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) = ( 𝑥 × 𝑦 ) )
58	57	mpompt	⊢ ( 𝑧 ∈ ( 𝑅 × 𝑆 ) ↦ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
59	58	eqcomi	⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑧 ∈ ( 𝑅 × 𝑆 ) ↦ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) )
60		eleq2	⊢ ( 𝑡 = ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) → ( 𝑝 ∈ 𝑡 ↔ 𝑝 ∈ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ) )
61		sseq1	⊢ ( 𝑡 = ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) → ( 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ↔ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
62	60 61	anbi12d	⊢ ( 𝑡 = ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) → ( ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ( 𝑝 ∈ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∧ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
63	59 62	rexrnmptw	⊢ ( ∀ 𝑧 ∈ ( 𝑅 × 𝑆 ) ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∈ V → ( ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ∃ 𝑧 ∈ ( 𝑅 × 𝑆 ) ( 𝑝 ∈ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∧ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
64	52 63	ax-mp	⊢ ( ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ∃ 𝑧 ∈ ( 𝑅 × 𝑆 ) ( 𝑝 ∈ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∧ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
65	57	eleq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ↔ 𝑝 ∈ ( 𝑥 × 𝑦 ) ) )
66	57	sseq1d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ↔ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
67	65 66	anbi12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑝 ∈ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∧ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
68	67	rexxp	⊢ ( ∃ 𝑧 ∈ ( 𝑅 × 𝑆 ) ( 𝑝 ∈ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ∧ ( ( 1^st ‘ 𝑧 ) × ( 2^nd ‘ 𝑧 ) ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
69	48 64 68	3bitri	⊢ ( ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) )
70	47 69	bitrdi	⊢ ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ( ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
71	44 70	raleqbidv	⊢ ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ( ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ↔ ∀ 𝑝 ∈ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑐 ) × ( 𝑏 ∩ 𝑑 ) ) ) ) )
72	41 71	syl5ibrcom	⊢ ( ( ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ( ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
73	72	rexlimdvva	⊢ ( ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) → ( ∃ 𝑏 ∈ 𝑆 ∃ 𝑑 ∈ 𝑆 ( 𝑢 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = ( 𝑐 × 𝑑 ) ) → ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
74	17 73	syl5bir	⊢ ( ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅 ) ) → ( ( ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) ∧ ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) ) → ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
75	74	rexlimdvva	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → ( ∃ 𝑎 ∈ 𝑅 ∃ 𝑐 ∈ 𝑅 ( ∃ 𝑏 ∈ 𝑆 𝑢 = ( 𝑎 × 𝑏 ) ∧ ∃ 𝑑 ∈ 𝑆 𝑣 = ( 𝑐 × 𝑑 ) ) → ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
76	16 75	syl5bi	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
77	76	ralrimivv	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
78	1	txbasex	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → 𝐵 ∈ V )
79		isbasis2g	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ TopBases ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
80	78 79	syl	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → ( 𝐵 ∈ TopBases ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑝 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
81	77 80	mpbird	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → 𝐵 ∈ TopBases )

Metamath Proof Explorer

Theorem txbas

Proof