This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ptopn

Description: A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

		Ref	Expression
	Hypotheses	ptopn.1	$⊢ φ \to A \in V$
		ptopn.2	$⊢ φ \to F : A ⟶ Top$
		ptopn.3	$⊢ φ \to W \in Fin$
		ptopn.4	$⊢ (φ \land k \in A) \to S \in F (k)$
		ptopn.5	$⊢ (φ \land k \in (A ∖ W)) \to S = ⋃ F (k)$
	Assertion	ptopn	$⊢ φ \to \underset{k \in A}{⨉} S \in \prod_{𝑡} (F)$

Proof

Step	Hyp	Ref	Expression
1		ptopn.1	$⊢ φ \to A \in V$
2		ptopn.2	$⊢ φ \to F : A ⟶ Top$
3		ptopn.3	$⊢ φ \to W \in Fin$
4		ptopn.4	$⊢ (φ \land k \in A) \to S \in F (k)$
5		ptopn.5	$⊢ (φ \land k \in (A ∖ W)) \to S = ⋃ F (k)$
6		eqid	$⊢ \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
7	6	ptbas	$⊢ (A \in V \land F : A ⟶ Top) \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases$
8	1 2 7	syl2anc	$⊢ φ \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases$
9		bastg	$⊢ \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \subseteq topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
10	8 9	syl	$⊢ φ \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \subseteq topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
11	2	ffnd	$⊢ φ \to F Fn A$
12	6	ptval	$⊢ (A \in V \land F Fn A) \to \prod_{𝑡} (F) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
13	1 11 12	syl2anc	$⊢ φ \to \prod_{𝑡} (F) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
14	10 13	sseqtrrd	$⊢ φ \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \subseteq \prod_{𝑡} (F)$
15	6 1 3 4 5	elptr2	$⊢ φ \to \underset{k \in A}{⨉} S \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
16	14 15	sseldd	$⊢ φ \to \underset{k \in A}{⨉} S \in \prod_{𝑡} (F)$