Metamath Proof Explorer

Theorem ptuni

Description: The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

		Ref	Expression
	Hypothesis	ptuni.1	$⊢ J = \prod_{𝑡} (F)$
	Assertion	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{x \in A}{⨉} ⋃ F (x) = ⋃ J$

Proof

Step	Hyp	Ref	Expression
1		ptuni.1	$⊢ J = \prod_{𝑡} (F)$
2		eqid	$⊢ \{k \| \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 k = \underset{y \in A}{⨉} g (y))\} = \{k \| \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 k = \underset{y \in A}{⨉} g (y))\}$
3	2	ptbas	$⊢ (A \in V \land F : A ⟶ Top) \to \{k \| \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 k = \underset{y \in A}{⨉} g (y))\} \in TopBases$
4		unitg	$⊢ \{k \| \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 k = \underset{y \in A}{⨉} g (y))\} \in TopBases \to ⋃ topGen (\{k \| \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 k = \underset{y \in A}{⨉} g (y))\}) = ⋃ \{k \| \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 k = \underset{y \in A}{⨉} g (y))\}$
5	3 4	syl	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ topGen (\{k \| \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 k = \underset{y \in A}{⨉} g (y))\}) = ⋃ \{k \| \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 k = \underset{y \in A}{⨉} g (y))\}$
6		ffn	$⊢ F : A ⟶ Top \to F Fn A$
7	2	ptval	$⊢ (A \in V \land F Fn A) \to \prod_{𝑡} (F) = topGen (\{k \| \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 k = \underset{y \in A}{⨉} g (y))\})$
8	6 7	sylan2	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) = topGen (\{k \| \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 k = \underset{y \in A}{⨉} g (y))\})$
9	1 8	syl5eq	$⊢ (A \in V \land F : A ⟶ Top) \to J = topGen (\{k \| \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 k = \underset{y \in A}{⨉} g (y))\})$
10	9	unieqd	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ J = ⋃ topGen (\{k \| \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 k = \underset{y \in A}{⨉} g (y))\})$
11	2	ptuni2	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{x \in A}{⨉} ⋃ F (x) = ⋃ \{k \| \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 k = \underset{y \in A}{⨉} g (y))\}$
12	5 10 11	3eqtr4rd	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{x \in A}{⨉} ⋃ F (x) = ⋃ J$