ptunimpt

Description: Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015)

		Ref	Expression
	Hypothesis	ptunimpt.j	$⊢ J = \prod_{𝑡} ((x \in A ⟼ K))$
	Assertion	ptunimpt	$⊢ (A \in V \land \forall x \in A K \in Top) \to \underset{x \in A}{⨉} ⋃ K = ⋃ J$

Proof

Step	Hyp	Ref	Expression
1		ptunimpt.j	$⊢ J = \prod_{𝑡} ((x \in A ⟼ K))$
2		eqid	$⊢ (x \in A ⟼ K) = (x \in A ⟼ K)$
3	2	fvmpt2	$⊢ (x \in A \land K \in Top) \to (x \in A ⟼ K) (x) = K$
4	3	eqcomd	$⊢ (x \in A \land K \in Top) \to K = (x \in A ⟼ K) (x)$
5	4	unieqd	$⊢ (x \in A \land K \in Top) \to ⋃ K = ⋃ (x \in A ⟼ K) (x)$
6	5	ralimiaa	$⊢ \forall x \in A K \in Top \to \forall x \in A ⋃ K = ⋃ (x \in A ⟼ K) (x)$
7	6	adantl	$⊢ (A \in V \land \forall x \in A K \in Top) \to \forall x \in A ⋃ K = ⋃ (x \in A ⟼ K) (x)$
8		ixpeq2	$⊢ \forall x \in A ⋃ K = ⋃ (x \in A ⟼ K) (x) \to \underset{x \in A}{⨉} ⋃ K = \underset{x \in A}{⨉} ⋃ (x \in A ⟼ K) (x)$
9	7 8	syl	$⊢ (A \in V \land \forall x \in A K \in Top) \to \underset{x \in A}{⨉} ⋃ K = \underset{x \in A}{⨉} ⋃ (x \in A ⟼ K) (x)$
10		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ K) (y)$
11	10	nfuni	$⊢ \underline{Ⅎ} x ⋃ (x \in A ⟼ K) (y)$
12		nfcv	$⊢ \underline{Ⅎ} y ⋃ (x \in A ⟼ K) (x)$
13		fveq2	$⊢ y = x \to (x \in A ⟼ K) (y) = (x \in A ⟼ K) (x)$
14	13	unieqd	$⊢ y = x \to ⋃ (x \in A ⟼ K) (y) = ⋃ (x \in A ⟼ K) (x)$
15	11 12 14	cbvixp	$⊢ \underset{y \in A}{⨉} ⋃ (x \in A ⟼ K) (y) = \underset{x \in A}{⨉} ⋃ (x \in A ⟼ K) (x)$
16	9 15	eqtr4di	$⊢ (A \in V \land \forall x \in A K \in Top) \to \underset{x \in A}{⨉} ⋃ K = \underset{y \in A}{⨉} ⋃ (x \in A ⟼ K) (y)$
17	2	fmpt	$⊢ \forall x \in A K \in Top \leftrightarrow (x \in A ⟼ K) : A ⟶ Top$
18	1	ptuni	$⊢ (A \in V \land (x \in A ⟼ K) : A ⟶ Top) \to \underset{y \in A}{⨉} ⋃ (x \in A ⟼ K) (y) = ⋃ J$
19	17 18	sylan2b	$⊢ (A \in V \land \forall x \in A K \in Top) \to \underset{y \in A}{⨉} ⋃ (x \in A ⟼ K) (y) = ⋃ J$
20	16 19	eqtrd	$⊢ (A \in V \land \forall x \in A K \in Top) \to \underset{x \in A}{⨉} ⋃ K = ⋃ J$

Metamath Proof Explorer

Theorem ptunimpt

Proof