Metamath Proof Explorer

Theorem ptcnp

Description: If every projection of a function is continuous at D , then the function itself is continuous at D into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses ptcnp.2 ⊢ 𝐾 = ( ∏t ‘ 𝐹 )
ptcnp.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
ptcnp.4 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
ptcnp.5 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
ptcnp.6 ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
ptcnp.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) )
Assertion ptcnp ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 ptcnp.2 ⊢ 𝐾 = ( ∏t ‘ 𝐹 )
2 ptcnp.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 ptcnp.4 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 ptcnp.5 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
5 ptcnp.6 ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
6 ptcnp.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
8 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
9 toptopon2 ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ Top ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
10 8 9 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
11 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
12 7 10 6 11 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
13 12 fvmptelrn ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
14 13 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
15 14 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
17 mptelixpg ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
19 15 18 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) )
20 19 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) )
21 df-3an ⊢ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) )
22 nfv ⊢ Ⅎ 𝑘 ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) )
23 nfv ⊢ Ⅎ 𝑘 ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) )
24 nfcv ⊢ Ⅎ 𝑘 𝑋
25 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐼 ↦ 𝐴 )
26 24 25 nfmpt ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) )
27 nfcv ⊢ Ⅎ 𝑘 𝐷
28 26 27 nffv ⊢ Ⅎ 𝑘 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 )
29 28 nfel1 ⊢ Ⅎ 𝑘 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 )
30 23 29 nfan ⊢ Ⅎ 𝑘 ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) )
31 22 30 nfan ⊢ Ⅎ 𝑘 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) )
32 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝑔 Fn 𝐼 )
33 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) )
34 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑘 ) )
35 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
36 34 35 eleq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑔 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) )
37 36 rspccva ⊢ ( ( ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
38 33 37 sylan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
39 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) )
40 39 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝑤 ∈ Fin )
41 39 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) )
42 35 unieqd ⊢ ( 𝑛 = 𝑘 → ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
43 34 42 eqeq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑔 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) )
44 43 rspccva ⊢ ( ( ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑤 ) ) → ( 𝑔 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
45 41 44 sylan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑤 ) ) → ( 𝑔 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
46 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) )
47 34 cbvixpv ⊢ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 )
48 46 47 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) )
49 1 2 3 4 5 6 31 32 38 40 45 48 ptcnplem ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) )
50 49 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ∧ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) )
51 50 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ∧ ( 𝑤 ∈ Fin ∧ ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
52 51 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) )
53 52 impr ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
54 21 53 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
55 eleq2 ⊢ ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) )
56 47 eqeq2i ⊢ ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ↔ 𝑓 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) )
57 56 biimpi ⊢ ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → 𝑓 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) )
58 57 sseq2d ⊢ ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) )
59 58 anbi2d ⊢ ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ( ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ↔ ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
60 59 rexbidv ⊢ ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ( ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ↔ ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
61 55 60 imbi12d ⊢ ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ( ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ↔ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) )
62 54 61 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ) )
63 62 expimpd ⊢ ( 𝜑 → ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ) )
64 63 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ) )
65 64 alrimiv ⊢ ( 𝜑 → ∀ 𝑓 ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ) )
66 eqeq1 ⊢ ( 𝑎 = 𝑓 → ( 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ↔ 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) )
67 66 anbi2d ⊢ ( 𝑎 = 𝑓 → ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) )
68 67 exbidv ⊢ ( 𝑎 = 𝑓 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) ) )
69 68 ralab ⊢ ( ∀ 𝑓 ∈ { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) } ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ↔ ∀ 𝑓 ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑓 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ) )
70 65 69 sylibr ⊢ ( 𝜑 → ∀ 𝑓 ∈ { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) } ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) )
71 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
72 eqid ⊢ { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) } = { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) }
73 72 ptval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 Fn 𝐼 ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) } ) )
74 3 71 73 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) = ( topGen ‘ { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) } ) )
75 1 74 eqtrid ⊢ ( 𝜑 → 𝐾 = ( topGen ‘ { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) } ) )
76 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) )
77 76 fveq2d ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) = ( ∏t ‘ ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
78 1 77 eqtrid ⊢ ( 𝜑 → 𝐾 = ( ∏t ‘ ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
79 10 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐼 ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
80 eqid ⊢ ( ∏t ‘ ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( ∏t ‘ ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) )
81 80 pttopon ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) ) → ( ∏t ‘ ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( TopOn ‘ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ) )
82 3 79 81 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( TopOn ‘ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ) )
83 78 82 eqeltrd ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ) )
84 2 75 83 5 tgcnp ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑓 ∈ { 𝑎 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑛 ∈ ( 𝐼 ∖ 𝑤 ) ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑎 = X 𝑛 ∈ 𝐼 ( 𝑔 ‘ 𝑛 ) ) } ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ 𝑓 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ 𝑓 ) ) ) ) )
85 20 70 84 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) )