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		fnex	$⊢ (G Fn A \land A \in V) \to G \in V$
5	2 3 4	syl2anc	$⊢ (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$
6		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)$
7		difeq2	$⊢ w = W \to A ∖ w = A ∖ W$
8	7	raleqdv	$⊢ w = W \to (\forall y \in (A ∖ w) G (y) = ⋃ F (y) \leftrightarrow \forall y \in (A ∖ W) G (y) = ⋃ F (y))$
9	8	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)$
10	9	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)$
11	2 6 10	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))$
12		fveq1	$⊢ h = G \to h (y) = G (y)$
13	12	eqcomd	$⊢ h = G \to G (y) = h (y)$
14	13	ixpeq2dv	$⊢ h = G \to \underset{y \in A}{⨉} G (y) = \underset{y \in A}{⨉} h (y)$
15	14	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)))$
16		fneq1	$⊢ h = G \to (h Fn A \leftrightarrow G Fn A)$
17	12	eleq1d	$⊢ h = G \to (h (y) \in F (y) \leftrightarrow G (y) \in F (y))$
18	17	ralbidv	$⊢ h = G \to (\forall y \in A h (y) \in F (y) \leftrightarrow \forall y \in A G (y) \in F (y))$
19	12	eqeq1d	$⊢ h = G \to (h (y) = ⋃ F (y) \leftrightarrow G (y) = ⋃ F (y))$
20	19	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))$
21	16 18 20	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)))$
22	15 21	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)))$
23	5 11 22	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))$
24	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))$
25	23 24	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