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	|- ( ph -> A e. V )
	ptopn2.f	|- ( ph -> F : A --> Top )
	ptopn2.o	|- ( ph -> O e. ( F ` Y ) )
Assertion	ptopn2	|- ( ph -> X_ k e. A if ( k = Y , O , U. ( F ` k ) ) e. ( Xt_ ` F ) )

Proof

Step	Hyp	Ref	Expression
1		ptopn2.a	|- ( ph -> A e. V )
2		ptopn2.f	|- ( ph -> F : A --> Top )
3		ptopn2.o	|- ( ph -> O e. ( F ` Y ) )
4		snfi	|- { Y } e. Fin
5	4	a1i	|- ( ph -> { Y } e. Fin )
6	3	adantr	|- ( ( ph /\ k e. A ) -> O e. ( F ` Y ) )
7		fveq2	|- ( k = Y -> ( F ` k ) = ( F ` Y ) )
8	7	eleq2d	|- ( k = Y -> ( O e. ( F ` k ) <-> O e. ( F ` Y ) ) )
9	6 8	syl5ibrcom	|- ( ( ph /\ k e. A ) -> ( k = Y -> O e. ( F ` k ) ) )
10	9	imp	|- ( ( ( ph /\ k e. A ) /\ k = Y ) -> O e. ( F ` k ) )
11	2	ffvelcdmda	|- ( ( ph /\ k e. A ) -> ( F ` k ) e. Top )
12		eqid	|- U. ( F ` k ) = U. ( F ` k )
13	12	topopn	|- ( ( F ` k ) e. Top -> U. ( F ` k ) e. ( F ` k ) )
14	11 13	syl	|- ( ( ph /\ k e. A ) -> U. ( F ` k ) e. ( F ` k ) )
15	14	adantr	|- ( ( ( ph /\ k e. A ) /\ -. k = Y ) -> U. ( F ` k ) e. ( F ` k ) )
16	10 15	ifclda	|- ( ( ph /\ k e. A ) -> if ( k = Y , O , U. ( F ` k ) ) e. ( F ` k ) )
17		eldifn	|- ( k e. ( A \ { Y } ) -> -. k e. { Y } )
18		velsn	|- ( k e. { Y } <-> k = Y )
19	17 18	sylnib	|- ( k e. ( A \ { Y } ) -> -. k = Y )
20	19	iffalsed	|- ( k e. ( A \ { Y } ) -> if ( k = Y , O , U. ( F ` k ) ) = U. ( F ` k ) )
21	20	adantl	|- ( ( ph /\ k e. ( A \ { Y } ) ) -> if ( k = Y , O , U. ( F ` k ) ) = U. ( F ` k ) )
22	1 2 5 16 21	ptopn	|- ( ph -> X_ k e. A if ( k = Y , O , U. ( F ` k ) ) e. ( Xt_ ` F ) )