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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ptopn2.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
	ptopn2.o	⊢ ( 𝜑 → 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) )
Assertion	ptopn2	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ∏t ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ptopn2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ptopn2.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
3		ptopn2.o	⊢ ( 𝜑 → 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) )
4		snfi	⊢ { 𝑌 } ∈ Fin
5	4	a1i	⊢ ( 𝜑 → { 𝑌 } ∈ Fin )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) )
7		fveq2	⊢ ( 𝑘 = 𝑌 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑌 ) )
8	7	eleq2d	⊢ ( 𝑘 = 𝑌 → ( 𝑂 ∈ ( 𝐹 ‘ 𝑘 ) ↔ 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) ) )
9	6 8	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑘 = 𝑌 → 𝑂 ∈ ( 𝐹 ‘ 𝑘 ) ) )
10	9	imp	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑘 = 𝑌 ) → 𝑂 ∈ ( 𝐹 ‘ 𝑘 ) )
11	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
12		eqid	⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
13	12	topopn	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ Top → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
14	11 13	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
15	14	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ¬ 𝑘 = 𝑌 ) → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
16	10 15	ifclda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 𝐹 ‘ 𝑘 ) )
17		eldifn	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) → ¬ 𝑘 ∈ { 𝑌 } )
18		velsn	⊢ ( 𝑘 ∈ { 𝑌 } ↔ 𝑘 = 𝑌 )
19	17 18	sylnib	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) → ¬ 𝑘 = 𝑌 )
20	19	iffalsed	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) → if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) = ∪ ( 𝐹 ‘ 𝑘 ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) ) → if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) = ∪ ( 𝐹 ‘ 𝑘 ) )
22	1 2 5 16 21	ptopn	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ∏t ‘ 𝐹 ) )