This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ptpjpre2

Description: The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypotheses ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
ptbasfi.2 ⊢ 𝑋 = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 )
Assertion ptpjpre2 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2 ptbasfi.2 ⊢ 𝑋 = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 )
3 2 ptpjpre1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) = X 𝑛 ∈ 𝐴 if ( 𝑛 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑛 ) ) )
4 simpll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → 𝐴 ∈ 𝑉 )
5 snfi ⊢ { 𝐼 } ∈ Fin
6 5 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → { 𝐼 } ∈ Fin )
7 simprr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) )
8 7 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) ∧ 𝑛 = 𝐼 ) → 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) )
9 simpr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) ∧ 𝑛 = 𝐼 ) → 𝑛 = 𝐼 )
10 9 fveq2d ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) ∧ 𝑛 = 𝐼 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝐼 ) )
11 8 10 eleqtrrd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) ∧ 𝑛 = 𝐼 ) → 𝑈 ∈ ( 𝐹 ‘ 𝑛 ) )
12 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → 𝐹 : 𝐴 ⟶ Top )
13 12 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) ∈ Top )
14 eqid ⊢ ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 )
15 14 topopn ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ Top → ∪ ( 𝐹 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) )
16 13 15 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) → ∪ ( 𝐹 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) )
17 16 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) ∧ ¬ 𝑛 = 𝐼 ) → ∪ ( 𝐹 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) )
18 11 17 ifclda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ 𝐴 ) → if ( 𝑛 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑛 ) ) ∈ ( 𝐹 ‘ 𝑛 ) )
19 eldifsni ⊢ ( 𝑛 ∈ ( 𝐴 ∖ { 𝐼 } ) → 𝑛 ≠ 𝐼 )
20 19 neneqd ⊢ ( 𝑛 ∈ ( 𝐴 ∖ { 𝐼 } ) → ¬ 𝑛 = 𝐼 )
21 20 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ ( 𝐴 ∖ { 𝐼 } ) ) → ¬ 𝑛 = 𝐼 )
22 21 iffalsed ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑛 ∈ ( 𝐴 ∖ { 𝐼 } ) ) → if ( 𝑛 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑛 ) ) = ∪ ( 𝐹 ‘ 𝑛 ) )
23 1 4 6 18 22 elptr2 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → X 𝑛 ∈ 𝐴 if ( 𝑛 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝐵 )
24 3 23 eqeltrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) ∈ 𝐵 )