elptr2

Description: A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

	Ref	Expression
Hypotheses	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))\}$
	elptr2.1	$⊢ φ \to A \in V$
	elptr2.2	$⊢ φ \to W \in Fin$
	elptr2.3	$⊢ (φ \land k \in A) \to S \in F (k)$
	elptr2.4	$⊢ (φ \land k \in (A ∖ W)) \to S = ⋃ F (k)$
Assertion	elptr2	$⊢ φ \to \underset{k \in A}{⨉} S \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		elptr2.1	$⊢ φ \to A \in V$
3		elptr2.2	$⊢ φ \to W \in Fin$
4		elptr2.3	$⊢ (φ \land k \in A) \to S \in F (k)$
5		elptr2.4	$⊢ (φ \land k \in (A ∖ W)) \to S = ⋃ F (k)$
6		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ S) (y)$
7		nfcv	$⊢ \underline{Ⅎ} y (k \in A ⟼ S) (k)$
8		fveq2	$⊢ y = k \to (k \in A ⟼ S) (y) = (k \in A ⟼ S) (k)$
9	6 7 8	cbvixp	$⊢ \underset{y \in A}{⨉} (k \in A ⟼ S) (y) = \underset{k \in A}{⨉} (k \in A ⟼ S) (k)$
10		simpr	$⊢ (φ \land k \in A) \to k \in A$
11		eqid	$⊢ (k \in A ⟼ S) = (k \in A ⟼ S)$
12	11	fvmpt2	$⊢ (k \in A \land S \in F (k)) \to (k \in A ⟼ S) (k) = S$
13	10 4 12	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ S) (k) = S$
14	13	ixpeq2dva	$⊢ φ \to \underset{k \in A}{⨉} (k \in A ⟼ S) (k) = \underset{k \in A}{⨉} S$
15	9 14	syl5eq	$⊢ φ \to \underset{y \in A}{⨉} (k \in A ⟼ S) (y) = \underset{k \in A}{⨉} S$
16	4	ralrimiva	$⊢ φ \to \forall k \in A S \in F (k)$
17	11	fnmpt	$⊢ \forall k \in A S \in F (k) \to (k \in A ⟼ S) Fn A$
18	16 17	syl	$⊢ φ \to (k \in A ⟼ S) Fn A$
19	13 4	eqeltrd	$⊢ (φ \land k \in A) \to (k \in A ⟼ S) (k) \in F (k)$
20	19	ralrimiva	$⊢ φ \to \forall k \in A (k \in A ⟼ S) (k) \in F (k)$
21	6	nfel1	$⊢ Ⅎ k (k \in A ⟼ S) (y) \in F (y)$
22		nfv	$⊢ Ⅎ y (k \in A ⟼ S) (k) \in F (k)$
23		fveq2	$⊢ y = k \to F (y) = F (k)$
24	8 23	eleq12d	$⊢ y = k \to ((k \in A ⟼ S) (y) \in F (y) \leftrightarrow (k \in A ⟼ S) (k) \in F (k))$
25	21 22 24	cbvralw	$⊢ \forall y \in A (k \in A ⟼ S) (y) \in F (y) \leftrightarrow \forall k \in A (k \in A ⟼ S) (k) \in F (k)$
26	20 25	sylibr	$⊢ φ \to \forall y \in A (k \in A ⟼ S) (y) \in F (y)$
27		eldifi	$⊢ k \in (A ∖ W) \to k \in A$
28	27 13	sylan2	$⊢ (φ \land k \in (A ∖ W)) \to (k \in A ⟼ S) (k) = S$
29	28 5	eqtrd	$⊢ (φ \land k \in (A ∖ W)) \to (k \in A ⟼ S) (k) = ⋃ F (k)$
30	29	ralrimiva	$⊢ φ \to \forall k \in (A ∖ W) (k \in A ⟼ S) (k) = ⋃ F (k)$
31	6	nfeq1	$⊢ Ⅎ k (k \in A ⟼ S) (y) = ⋃ F (y)$
32		nfv	$⊢ Ⅎ y (k \in A ⟼ S) (k) = ⋃ F (k)$
33	23	unieqd	$⊢ y = k \to ⋃ F (y) = ⋃ F (k)$
34	8 33	eqeq12d	$⊢ y = k \to ((k \in A ⟼ S) (y) = ⋃ F (y) \leftrightarrow (k \in A ⟼ S) (k) = ⋃ F (k))$
35	31 32 34	cbvralw	$⊢ \forall y \in (A ∖ W) (k \in A ⟼ S) (y) = ⋃ F (y) \leftrightarrow \forall k \in (A ∖ W) (k \in A ⟼ S) (k) = ⋃ F (k)$
36	30 35	sylibr	$⊢ φ \to \forall y \in (A ∖ W) (k \in A ⟼ S) (y) = ⋃ F (y)$
37	1	elptr	$⊢ (A \in V \land ((k \in A ⟼ S) Fn A \land \forall y \in A (k \in A ⟼ S) (y) \in F (y)) \land (W \in Fin \land \forall y \in (A ∖ W) (k \in A ⟼ S) (y) = ⋃ F (y))) \to \underset{y \in A}{⨉} (k \in A ⟼ S) (y) \in B$
38	2 18 26 3 36 37	syl122anc	$⊢ φ \to \underset{y \in A}{⨉} (k \in A ⟼ S) (y) \in B$
39	15 38	eqeltrrd	$⊢ φ \to \underset{k \in A}{⨉} S \in B$

Metamath Proof Explorer

Theorem elptr2

Proof