Theorem ptopn2

Description: A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Hypotheses	ptopn2.a	$$⊢\phi \to A\in V$$
	ptopn2.f	$$⊢\phi \to F:A⟶\mathrm{Top}$$
	ptopn2.o	$$⊢\phi \to O\in F\left(Y\right)$$
Assertion	ptopn2	$$⊢\phi \to \underset{k\in A}{⨉}if\left(k=Y,O,\bigcup F\left(k\right)\right)\in {\prod }_{𝑡}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		ptopn2.a	$$⊢\phi \to A\in V$$
2		ptopn2.f	$$⊢\phi \to F:A⟶\mathrm{Top}$$
3		ptopn2.o	$$⊢\phi \to O\in F\left(Y\right)$$
4		snfi	$$⊢\left\{Y\right\}\in \mathrm{Fin}$$
5	4	a1i	$$⊢\phi \to \left\{Y\right\}\in \mathrm{Fin}$$
6	3	adantr	$$⊢\left(\phi \wedge k\in A\right)\to O\in F\left(Y\right)$$
7		fveq2	$$⊢k=Y\to F\left(k\right)=F\left(Y\right)$$
8	7	eleq2d	$$⊢k=Y\to \left(O\in F\left(k\right)\leftrightarrow O\in F\left(Y\right)\right)$$
9	6 8	syl5ibrcom	$$⊢\left(\phi \wedge k\in A\right)\to \left(k=Y\to O\in F\left(k\right)\right)$$
10	9	imp	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge k=Y\right)\to O\in F\left(k\right)$$
11	2	ffvelcdmda	$$⊢\left(\phi \wedge k\in A\right)\to F\left(k\right)\in \mathrm{Top}$$
12		eqid	$$⊢\bigcup F\left(k\right)=\bigcup F\left(k\right)$$
13	12	topopn	$$⊢F\left(k\right)\in \mathrm{Top}\to \bigcup F\left(k\right)\in F\left(k\right)$$
14	11 13	syl	$$⊢\left(\phi \wedge k\in A\right)\to \bigcup F\left(k\right)\in F\left(k\right)$$
15	14	adantr	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge \neg k=Y\right)\to \bigcup F\left(k\right)\in F\left(k\right)$$
16	10 15	ifclda	$$⊢\left(\phi \wedge k\in A\right)\to if\left(k=Y,O,\bigcup F\left(k\right)\right)\in F\left(k\right)$$
17		eldifn	$$⊢k\in \left(A\setminus \left\{Y\right\}\right)\to \neg k\in \left\{Y\right\}$$
18		velsn	$$⊢k\in \left\{Y\right\}\leftrightarrow k=Y$$
19	17 18	sylnib	$$⊢k\in \left(A\setminus \left\{Y\right\}\right)\to \neg k=Y$$
20	19	iffalsed	$$⊢k\in \left(A\setminus \left\{Y\right\}\right)\to if\left(k=Y,O,\bigcup F\left(k\right)\right)=\bigcup F\left(k\right)$$
21	20	adantl	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{Y\right\}\right)\right)\to if\left(k=Y,O,\bigcup F\left(k\right)\right)=\bigcup F\left(k\right)$$
22	1 2 5 16 21	ptopn	$$⊢\phi \to \underset{k\in A}{⨉}if\left(k=Y,O,\bigcup F\left(k\right)\right)\in {\prod }_{𝑡}\left(F\right)$$