ptuni2

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

		Ref	Expression
	Hypothesis	ptbas.1	$⊢ B = \{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))\}$
	Assertion	ptuni2	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ B$

Proof

Step	Hyp	Ref	Expression
1		ptbas.1	$⊢ B = \{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))\}$
2	1	ptbasid	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) \in B$
3		elssuni	$⊢ \underset{k \in A}{⨉} ⋃ F (k) \in B \to \underset{k \in A}{⨉} ⋃ F (k) \subseteq ⋃ B$
4	2 3	syl	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) \subseteq ⋃ B$
5		simpr2	$⊢ ((A \in V \land F : A ⟶ Top) \land (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))) \to \forall y \in A g (y) \in F (y)$
6		elssuni	$⊢ g (y) \in F (y) \to g (y) \subseteq ⋃ F (y)$
7	6	ralimi	$⊢ \forall y \in A g (y) \in F (y) \to \forall y \in A g (y) \subseteq ⋃ F (y)$
8		ss2ixp	$⊢ \forall y \in A g (y) \subseteq ⋃ F (y) \to \underset{y \in A}{⨉} g (y) \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
9	5 7 8	3syl	$⊢ ((A \in V \land F : A ⟶ Top) \land (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))) \to \underset{y \in A}{⨉} g (y) \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
10		fveq2	$⊢ y = k \to F (y) = F (k)$
11	10	unieqd	$⊢ y = k \to ⋃ F (y) = ⋃ F (k)$
12	11	cbvixpv	$⊢ \underset{y \in A}{⨉} ⋃ F (y) = \underset{k \in A}{⨉} ⋃ F (k)$
13	9 12	sseqtrdi	$⊢ ((A \in V \land F : A ⟶ Top) \land (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))) \to \underset{y \in A}{⨉} g (y) \subseteq \underset{k \in A}{⨉} ⋃ F (k)$
14		velpw	$⊢ x \in 𝒫 \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow x \subseteq \underset{k \in A}{⨉} ⋃ F (k)$
15		sseq1	$⊢ x = \underset{y \in A}{⨉} g (y) \to (x \subseteq \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow \underset{y \in A}{⨉} g (y) \subseteq \underset{k \in A}{⨉} ⋃ F (k))$
16	14 15	bitrid	$⊢ x = \underset{y \in A}{⨉} g (y) \to (x \in 𝒫 \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow \underset{y \in A}{⨉} g (y) \subseteq \underset{k \in A}{⨉} ⋃ F (k))$
17	13 16	syl5ibrcom	$⊢ ((A \in V \land F : A ⟶ Top) \land (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))) \to (x = \underset{y \in A}{⨉} g (y) \to x \in 𝒫 \underset{k \in A}{⨉} ⋃ F (k))$
18	17	expimpd	$⊢ (A \in V \land F : A ⟶ Top) \to (((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)) \to x \in 𝒫 \underset{k \in A}{⨉} ⋃ F (k))$
19	18	exlimdv	$⊢ (A \in V \land F : A ⟶ Top) \to (\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)) \to x \in 𝒫 \underset{k \in A}{⨉} ⋃ F (k))$
20	19	abssdv	$⊢ (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))\} \subseteq 𝒫 \underset{k \in A}{⨉} ⋃ F (k)$
21	1 20	eqsstrid	$⊢ (A \in V \land F : A ⟶ Top) \to B \subseteq 𝒫 \underset{k \in A}{⨉} ⋃ F (k)$
22		sspwuni	$⊢ B \subseteq 𝒫 \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow ⋃ B \subseteq \underset{k \in A}{⨉} ⋃ F (k)$
23	21 22	sylib	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ B \subseteq \underset{k \in A}{⨉} ⋃ F (k)$
24	4 23	eqssd	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ B$

Metamath Proof Explorer

Theorem ptuni2

Proof