Metamath Proof Explorer

Theorem pttopon

Description: The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ptunimpt.j	$⊢ J = \prod_{𝑡} ((x \in A ⟼ K))$
2		topontop	$⊢ K \in TopOn (B) \to K \in Top$
3	2	ralimi	$⊢ \forall x \in A K \in TopOn (B) \to \forall x \in A K \in Top$
4		eqid	$⊢ (x \in A ⟼ K) = (x \in A ⟼ K)$
5	4	fmpt	$⊢ \forall x \in A K \in Top \leftrightarrow (x \in A ⟼ K) : A ⟶ Top$
6	3 5	sylib	$⊢ \forall x \in A K \in TopOn (B) \to (x \in A ⟼ K) : A ⟶ Top$
7		pttop	$⊢ (A \in V \land (x \in A ⟼ K) : A ⟶ Top) \to \prod_{𝑡} ((x \in A ⟼ K)) \in Top$
8	1 7	eqeltrid	$⊢ (A \in V \land (x \in A ⟼ K) : A ⟶ Top) \to J \in Top$
9	6 8	sylan2	$⊢ (A \in V \land \forall x \in A K \in TopOn (B)) \to J \in Top$
10		toponuni	$⊢ K \in TopOn (B) \to B = ⋃ K$
11	10	ralimi	$⊢ \forall x \in A K \in TopOn (B) \to \forall x \in A B = ⋃ K$
12		ixpeq2	$⊢ \forall x \in A B = ⋃ K \to \underset{x \in A}{⨉} B = \underset{x \in A}{⨉} ⋃ K$
13	11 12	syl	$⊢ \forall x \in A K \in TopOn (B) \to \underset{x \in A}{⨉} B = \underset{x \in A}{⨉} ⋃ K$
14	13	adantl	$⊢ (A \in V \land \forall x \in A K \in TopOn (B)) \to \underset{x \in A}{⨉} B = \underset{x \in A}{⨉} ⋃ K$
15	1	ptunimpt	$⊢ (A \in V \land \forall x \in A K \in Top) \to \underset{x \in A}{⨉} ⋃ K = ⋃ J$
16	3 15	sylan2	$⊢ (A \in V \land \forall x \in A K \in TopOn (B)) \to \underset{x \in A}{⨉} ⋃ K = ⋃ J$
17	14 16	eqtrd	$⊢ (A \in V \land \forall x \in A K \in TopOn (B)) \to \underset{x \in A}{⨉} B = ⋃ J$
18		istopon	$⊢ J \in TopOn (\underset{x \in A}{⨉} B) \leftrightarrow (J \in Top \land \underset{x \in A}{⨉} B = ⋃ J)$
19	9 17 18	sylanbrc	$⊢ (A \in V \land \forall x \in A K \in TopOn (B)) \to J \in TopOn (\underset{x \in A}{⨉} B)$