ptpjpre2

Description: The basis for a product topology is a basis. (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))\}$
	ptbasfi.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
Assertion	ptpjpre2	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to {(w \in X ⟼ w (I))}^{-1} [U] \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		ptbasfi.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
3	2	ptpjpre1	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to {(w \in X ⟼ w (I))}^{-1} [U] = \underset{n \in A}{⨉} if (n = I, U, ⋃ F (n))$
4		simpll	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to A \in V$
5		snfi	$⊢ \{I\} \in Fin$
6	5	a1i	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to \{I\} \in Fin$
7		simprr	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to U \in F (I)$
8	7	ad2antrr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \land n = I) \to U \in F (I)$
9		simpr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \land n = I) \to n = I$
10	9	fveq2d	$⊢ ((((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \land n = I) \to F (n) = F (I)$
11	8 10	eleqtrrd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \land n = I) \to U \in F (n)$
12		simplr	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to F : A ⟶ Top$
13	12	ffvelcdmda	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \to F (n) \in Top$
14		eqid	$⊢ ⋃ F (n) = ⋃ F (n)$
15	14	topopn	$⊢ F (n) \in Top \to ⋃ F (n) \in F (n)$
16	13 15	syl	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \to ⋃ F (n) \in F (n)$
17	16	adantr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \land \neg n = I) \to ⋃ F (n) \in F (n)$
18	11 17	ifclda	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in A) \to if (n = I, U, ⋃ F (n)) \in F (n)$
19		eldifsni	$⊢ n \in (A ∖ \{I\}) \to n \neq I$
20	19	neneqd	$⊢ n \in (A ∖ \{I\}) \to \neg n = I$
21	20	adantl	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in (A ∖ \{I\})) \to \neg n = I$
22	21	iffalsed	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land n \in (A ∖ \{I\})) \to if (n = I, U, ⋃ F (n)) = ⋃ F (n)$
23	1 4 6 18 22	elptr2	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to \underset{n \in A}{⨉} if (n = I, U, ⋃ F (n)) \in B$
24	3 23	eqeltrd	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to {(w \in X ⟼ w (I))}^{-1} [U] \in B$

Metamath Proof Explorer

Theorem ptpjpre2

Proof