elptr

Description: A basic open set in 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	elptr	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to \underset{y \in A}{⨉} G (y) \in 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		simp2l	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to G Fn A$
3		simp1	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to A \in V$
4	2 3	fnexd	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to G \in V$
5		simp2r	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to \forall y \in A G (y) \in F (y)$
6		difeq2	$⊢ w = W \to A ∖ w = A ∖ W$
7	6	raleqdv	$⊢ w = W \to (\forall y \in (A ∖ w) G (y) = ⋃ F (y) \leftrightarrow \forall y \in (A ∖ W) G (y) = ⋃ F (y))$
8	7	rspcev	$⊢ (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y)) \to \exists w \in Fin \forall y \in (A ∖ w) G (y) = ⋃ F (y)$
9	8	3ad2ant3	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to \exists w \in Fin \forall y \in (A ∖ w) G (y) = ⋃ F (y)$
10	2 5 9	3jca	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to (G Fn A \land \forall y \in A G (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) G (y) = ⋃ F (y))$
11		fveq1	$⊢ h = G \to h (y) = G (y)$
12	11	eqcomd	$⊢ h = G \to G (y) = h (y)$
13	12	ixpeq2dv	$⊢ h = G \to \underset{y \in A}{⨉} G (y) = \underset{y \in A}{⨉} h (y)$
14	13	biantrud	$⊢ h = G \to ((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)) \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 \underset{y \in A}{⨉} G (y) = \underset{y \in A}{⨉} h (y)))$
15		fneq1	$⊢ h = G \to (h Fn A \leftrightarrow G Fn A)$
16	11	eleq1d	$⊢ h = G \to (h (y) \in F (y) \leftrightarrow G (y) \in F (y))$
17	16	ralbidv	$⊢ h = G \to (\forall y \in A h (y) \in F (y) \leftrightarrow \forall y \in A G (y) \in F (y))$
18	11	eqeq1d	$⊢ h = G \to (h (y) = ⋃ F (y) \leftrightarrow G (y) = ⋃ F (y))$
19	18	rexralbidv	$⊢ h = G \to (\exists w \in Fin \forall y \in (A ∖ w) h (y) = ⋃ F (y) \leftrightarrow \exists w \in Fin \forall y \in (A ∖ w) G (y) = ⋃ F (y))$
20	15 17 19	3anbi123d	$⊢ h = G \to ((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)) \leftrightarrow (G Fn A \land \forall y \in A G (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) G (y) = ⋃ F (y)))$
21	14 20	bitr3d	$⊢ h = G \to (((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 \underset{y \in A}{⨉} G (y) = \underset{y \in A}{⨉} h (y)) \leftrightarrow (G Fn A \land \forall y \in A G (y) \in F (y) \land \exists w \in Fin \forall y \in (A ∖ w) G (y) = ⋃ F (y)))$
22	4 10 21	spcedv	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to \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 \underset{y \in A}{⨉} G (y) = \underset{y \in A}{⨉} h (y))$
23	1	elpt	$⊢ \underset{y \in A}{⨉} G (y) \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 \underset{y \in A}{⨉} G (y) = \underset{y \in A}{⨉} h (y))$
24	22 23	sylibr	$⊢ (A \in V \land (G Fn A \land \forall y \in A G (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) G (y) = ⋃ F (y))) \to \underset{y \in A}{⨉} G (y) \in B$

Metamath Proof Explorer

Theorem elptr

Proof