elpt

Description: Elementhood in the bases of a 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	elpt	$⊢ S \in B \leftrightarrow \exists h ((h Fn A \land \forall y \in A h (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y)) \land S = \underset{y \in A}{⨉} h (y))$

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	eleq2i	$⊢ S \in B \leftrightarrow 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))\}$
3		simpr	$⊢ ((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 S = \underset{y \in A}{⨉} g (y)) \to S = \underset{y \in A}{⨉} g (y)$
4		ixpexg	$⊢ \forall y \in A g (y) \in V \to \underset{y \in A}{⨉} g (y) \in V$
5		fvexd	$⊢ y \in A \to g (y) \in V$
6	4 5	mprg	$⊢ \underset{y \in A}{⨉} g (y) \in V$
7	3 6	eqeltrdi	$⊢ ((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 S = \underset{y \in A}{⨉} g (y)) \to S \in V$
8	7	exlimiv	$⊢ \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 S = \underset{y \in A}{⨉} g (y)) \to S \in V$
9		eqeq1	$⊢ x = S \to (x = \underset{y \in A}{⨉} g (y) \leftrightarrow S = \underset{y \in A}{⨉} g (y))$
10	9	anbi2d	$⊢ x = S \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)) \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 S = \underset{y \in A}{⨉} g (y)))$
11	10	exbidv	$⊢ x = S \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)) \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 S = \underset{y \in A}{⨉} g (y)))$
12	8 11	elab3	$⊢ 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))\} \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 S = \underset{y \in A}{⨉} g (y))$
13		fneq1	$⊢ g = h \to (g Fn A \leftrightarrow h Fn A)$
14		fveq1	$⊢ g = h \to g (y) = h (y)$
15	14	eleq1d	$⊢ g = h \to (g (y) \in F (y) \leftrightarrow h (y) \in F (y))$
16	15	ralbidv	$⊢ g = h \to (\forall y \in A g (y) \in F (y) \leftrightarrow \forall y \in A h (y) \in F (y))$
17	14	eqeq1d	$⊢ g = h \to (g (y) = ⋃ F (y) \leftrightarrow h (y) = ⋃ F (y))$
18	17	rexralbidv	$⊢ g = h \to (\exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y) \leftrightarrow \exists z \in Fin \forall y \in (A ∖ z) h (y) = ⋃ F (y))$
19		difeq2	$⊢ z = w \to A ∖ z = A ∖ w$
20	19	raleqdv	$⊢ z = w \to (\forall y \in (A ∖ z) h (y) = ⋃ F (y) \leftrightarrow \forall y \in (A ∖ w) h (y) = ⋃ F (y))$
21	20	cbvrexvw	$⊢ \exists z \in Fin \forall y \in (A ∖ z) h (y) = ⋃ F (y) \leftrightarrow \exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y)$
22	18 21	bitrdi	$⊢ g = h \to (\exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y) \leftrightarrow \exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y))$
23	13 16 22	3anbi123d	$⊢ g = h \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)) \leftrightarrow (h Fn A \land \forall y \in A h (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y)))$
24	14	ixpeq2dv	$⊢ g = h \to \underset{y \in A}{⨉} g (y) = \underset{y \in A}{⨉} h (y)$
25	24	eqeq2d	$⊢ g = h \to (S = \underset{y \in A}{⨉} g (y) \leftrightarrow S = \underset{y \in A}{⨉} h (y))$
26	23 25	anbi12d	$⊢ g = h \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 S = \underset{y \in A}{⨉} g (y)) \leftrightarrow ((h Fn A \land \forall y \in A h (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y)) \land S = \underset{y \in A}{⨉} h (y)))$
27	26	cbvexvw	$⊢ \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 S = \underset{y \in A}{⨉} g (y)) \leftrightarrow \exists h ((h Fn A \land \forall y \in A h (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y)) \land S = \underset{y \in A}{⨉} h (y))$
28	2 12 27	3bitri	$⊢ S \in B \leftrightarrow \exists h ((h Fn A \land \forall y \in A h (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y)) \land S = \underset{y \in A}{⨉} h (y))$

Metamath Proof Explorer

Theorem elpt

Proof