ptval2

Description: The value of the product topology function. (Contributed by Mario Carneiro, 7-Feb-2015)

	Ref	Expression
Hypotheses	ptval2.1	$⊢ J = \prod_{𝑡} (F)$
	ptval2.2	$⊢ X = ⋃ J$
	ptval2.3	$⊢ G = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
Assertion	ptval2	$⊢ (A \in V \land F : A ⟶ Top) \to J = topGen (fi (\{X\} \cup ran G))$

Proof

Step	Hyp	Ref	Expression
1		ptval2.1	$⊢ J = \prod_{𝑡} (F)$
2		ptval2.2	$⊢ X = ⋃ J$
3		ptval2.3	$⊢ G = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
4		ffn	$⊢ F : A ⟶ Top \to F Fn A$
5		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))\}$
6	5	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))\})$
7	1 6	syl5eq	$⊢ (A \in V \land F Fn A) \to J = 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))\})$
8	4 7	sylan2	$⊢ (A \in V \land F : A ⟶ Top) \to J = 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))\})$
9		eqid	$⊢ \underset{n \in A}{⨉} ⋃ F (n) = \underset{n \in A}{⨉} ⋃ F (n)$
10	5 9	ptbasfi	$⊢ (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))\} = fi (\{\underset{n \in A}{⨉} ⋃ F (n)\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]))$
11	1	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{n \in A}{⨉} ⋃ F (n) = ⋃ J$
12	11 2	eqtr4di	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{n \in A}{⨉} ⋃ F (n) = X$
13	12	sneqd	$⊢ (A \in V \land F : A ⟶ Top) \to \{\underset{n \in A}{⨉} ⋃ F (n)\} = \{X\}$
14	12	3ad2ant1	$⊢ ((A \in V \land F : A ⟶ Top) \land k \in A \land u \in F (k)) \to \underset{n \in A}{⨉} ⋃ F (n) = X$
15	14	mpteq1d	$⊢ ((A \in V \land F : A ⟶ Top) \land k \in A \land u \in F (k)) \to (w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k)) = (w \in X ⟼ w (k))$
16	15	cnveqd	$⊢ ((A \in V \land F : A ⟶ Top) \land k \in A \land u \in F (k)) \to {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} = {(w \in X ⟼ w (k))}^{-1}$
17	16	imaeq1d	$⊢ ((A \in V \land F : A ⟶ Top) \land k \in A \land u \in F (k)) \to {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u] = {(w \in X ⟼ w (k))}^{-1} [u]$
18	17	mpoeq3dva	$⊢ (A \in V \land F : A ⟶ Top) \to (k \in A, u \in F (k) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]) = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
19	18 3	eqtr4di	$⊢ (A \in V \land F : A ⟶ Top) \to (k \in A, u \in F (k) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]) = G$
20	19	rneqd	$⊢ (A \in V \land F : A ⟶ Top) \to ran (k \in A, u \in F (k) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]) = ran G$
21	13 20	uneq12d	$⊢ (A \in V \land F : A ⟶ Top) \to \{\underset{n \in A}{⨉} ⋃ F (n)\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]) = \{X\} \cup ran G$
22	21	fveq2d	$⊢ (A \in V \land F : A ⟶ Top) \to fi (\{\underset{n \in A}{⨉} ⋃ F (n)\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u])) = fi (\{X\} \cup ran G)$
23	10 22	eqtrd	$⊢ (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))\} = fi (\{X\} \cup ran G)$
24	23	fveq2d	$⊢ (A \in V \land F : A ⟶ Top) \to 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))\}) = topGen (fi (\{X\} \cup ran G))$
25	8 24	eqtrd	$⊢ (A \in V \land F : A ⟶ Top) \to J = topGen (fi (\{X\} \cup ran G))$

Metamath Proof Explorer

Theorem ptval2

Proof