ptval

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

		Ref	Expression
	Hypothesis	ptval.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	ptval	$⊢ (A \in V \land F Fn A) \to \prod_{𝑡} (F) = topGen (B)$

Proof

Step	Hyp	Ref	Expression
1		ptval.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		df-pt	$⊢ \prod_{𝑡} = (f \in V ⟼ topGen (\{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\}))$
3		simpr	$⊢ ((A \in V \land F Fn A) \land f = F) \to f = F$
4	3	dmeqd	$⊢ ((A \in V \land F Fn A) \land f = F) \to dom f = dom F$
5		fndm	$⊢ F Fn A \to dom F = A$
6	5	ad2antlr	$⊢ ((A \in V \land F Fn A) \land f = F) \to dom F = A$
7	4 6	eqtrd	$⊢ ((A \in V \land F Fn A) \land f = F) \to dom f = A$
8	7	fneq2d	$⊢ ((A \in V \land F Fn A) \land f = F) \to (g Fn dom f \leftrightarrow g Fn A)$
9	3	fveq1d	$⊢ ((A \in V \land F Fn A) \land f = F) \to f (y) = F (y)$
10	9	eleq2d	$⊢ ((A \in V \land F Fn A) \land f = F) \to (g (y) \in f (y) \leftrightarrow g (y) \in F (y))$
11	7 10	raleqbidv	$⊢ ((A \in V \land F Fn A) \land f = F) \to (\forall y \in dom f g (y) \in f (y) \leftrightarrow \forall y \in A g (y) \in F (y))$
12	7	difeq1d	$⊢ ((A \in V \land F Fn A) \land f = F) \to dom f ∖ z = A ∖ z$
13	9	unieqd	$⊢ ((A \in V \land F Fn A) \land f = F) \to ⋃ f (y) = ⋃ F (y)$
14	13	eqeq2d	$⊢ ((A \in V \land F Fn A) \land f = F) \to (g (y) = ⋃ f (y) \leftrightarrow g (y) = ⋃ F (y))$
15	12 14	raleqbidv	$⊢ ((A \in V \land F Fn A) \land f = F) \to (\forall y \in (dom f ∖ z) g (y) = ⋃ f (y) \leftrightarrow \forall y \in (A ∖ z) g (y) = ⋃ F (y))$
16	15	rexbidv	$⊢ ((A \in V \land F Fn A) \land f = F) \to (\exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y) \leftrightarrow \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))$
17	8 11 16	3anbi123d	$⊢ ((A \in V \land F Fn A) \land f = F) \to ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \leftrightarrow (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)))$
18	7	ixpeq1d	$⊢ ((A \in V \land F Fn A) \land f = F) \to \underset{y \in dom f}{⨉} g (y) = \underset{y \in A}{⨉} g (y)$
19	18	eqeq2d	$⊢ ((A \in V \land F Fn A) \land f = F) \to (x = \underset{y \in dom f}{⨉} g (y) \leftrightarrow x = \underset{y \in A}{⨉} g (y))$
20	17 19	anbi12d	$⊢ ((A \in V \land F Fn A) \land f = F) \to (((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y)) \leftrightarrow ((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)))$
21	20	exbidv	$⊢ ((A \in V \land F Fn A) \land f = F) \to (\exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y)) \leftrightarrow \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)))$
22	21	abbidv	$⊢ ((A \in V \land F Fn A) \land f = F) \to \{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} 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))\}$
23	22 1	eqtr4di	$⊢ ((A \in V \land F Fn A) \land f = F) \to \{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\} = B$
24	23	fveq2d	$⊢ ((A \in V \land F Fn A) \land f = F) \to topGen (\{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\}) = topGen (B)$
25		fnex	$⊢ (F Fn A \land A \in V) \to F \in V$
26	25	ancoms	$⊢ (A \in V \land F Fn A) \to F \in V$
27		fvexd	$⊢ (A \in V \land F Fn A) \to topGen (B) \in V$
28	2 24 26 27	fvmptd2	$⊢ (A \in V \land F Fn A) \to \prod_{𝑡} (F) = topGen (B)$

Metamath Proof Explorer

Theorem ptval

Proof