Metamath Proof Explorer

Theorem ptrest

Description: Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019)

Ref Expression
Hypotheses ptrest.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ptrest.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
ptrest.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ 𝑊 )
Assertion ptrest ( 𝜑 → ( ( ∏t ‘ 𝐹 ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 ptrest.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 ptrest.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
3 ptrest.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ 𝑊 )
4 firest ⊢ ( fi ‘ ( ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) ) = ( ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 )
5 snex ⊢ { ∪ ( ∏t ‘ 𝐹 ) } ∈ V
6 fvex ⊢ ( 𝐹 ‘ 𝑢 ) ∈ V
7 6 rgenw ⊢ ∀ 𝑢 ∈ 𝐴 ( 𝐹 ‘ 𝑢 ) ∈ V
8 eqid ⊢ ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) )
9 8 mpoexxg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑢 ∈ 𝐴 ( 𝐹 ‘ 𝑢 ) ∈ V ) → ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ∈ V )
10 1 7 9 sylancl ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ∈ V )
11 rnexg ⊢ ( ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ∈ V → ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ∈ V )
12 10 11 syl ⊢ ( 𝜑 → ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ∈ V )
13 unexg ⊢ ( ( { ∪ ( ∏t ‘ 𝐹 ) } ∈ V ∧ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ∈ V ) → ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ∈ V )
14 5 12 13 sylancr ⊢ ( 𝜑 → ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ∈ V )
15 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑆 ∈ 𝑊 )
16 ixpexg ⊢ ( ∀ 𝑘 ∈ 𝐴 𝑆 ∈ 𝑊 → X 𝑘 ∈ 𝐴 𝑆 ∈ V )
17 15 16 syl ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 𝑆 ∈ V )
18 restval ⊢ ( ( ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ∈ V ∧ X 𝑘 ∈ 𝐴 𝑆 ∈ V ) → ( ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ran ( 𝑥 ∈ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
19 14 17 18 syl2anc ⊢ ( 𝜑 → ( ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ran ( 𝑥 ∈ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
20 mptun ⊢ ( 𝑥 ∈ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ( ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ∪ ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
21 20 rneqi ⊢ ran ( 𝑥 ∈ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ran ( ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ∪ ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
22 rnun ⊢ ran ( ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ∪ ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ) = ( ran ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ∪ ran ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
23 21 22 eqtri ⊢ ran ( 𝑥 ∈ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ( ran ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ∪ ran ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
24 elsni ⊢ ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } → 𝑥 = ∪ ( ∏t ‘ 𝐹 ) )
25 24 ineq1d ⊢ ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } → ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) = ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) )
26 25 mpteq2ia ⊢ ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) )
27 fvex ⊢ ( ∏t ‘ 𝐹 ) ∈ V
28 27 uniex ⊢ ∪ ( ∏t ‘ 𝐹 ) ∈ V
29 28 inex1 ⊢ ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ∈ V
30 fmptsn ⊢ ( ( ∪ ( ∏t ‘ 𝐹 ) ∈ V ∧ ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ∈ V ) → { ⟨ ∪ ( ∏t ‘ 𝐹 ) , ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ⟩ } = ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
31 28 29 30 mp2an ⊢ { ⟨ ∪ ( ∏t ‘ 𝐹 ) , ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ⟩ } = ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) )
32 26 31 eqtr4i ⊢ ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = { ⟨ ∪ ( ∏t ‘ 𝐹 ) , ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ⟩ }
33 32 rneqi ⊢ ran ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ran { ⟨ ∪ ( ∏t ‘ 𝐹 ) , ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ⟩ }
34 28 rnsnop ⊢ ran { ⟨ ∪ ( ∏t ‘ 𝐹 ) , ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ⟩ } = { ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) }
35 33 34 eqtri ⊢ ran ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = { ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) }
36 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
37 inss1 ⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) ⊆ ∪ ( 𝐹 ‘ 𝑘 )
38 eqid ⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
39 38 restuni ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ Top ∧ ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) = ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) ) )
40 36 37 39 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) = ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) ) )
41 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
42 38 restin ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ V ∧ 𝑆 ∈ 𝑊 ) → ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = ( ( 𝐹 ‘ 𝑘 ) ↾t ( 𝑆 ∩ ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
43 41 3 42 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = ( ( 𝐹 ‘ 𝑘 ) ↾t ( 𝑆 ∩ ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
44 incom ⊢ ( 𝑆 ∩ ∪ ( 𝐹 ‘ 𝑘 ) ) = ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 )
45 44 oveq2i ⊢ ( ( 𝐹 ‘ 𝑘 ) ↾t ( 𝑆 ∩ ∪ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) ↾t ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) )
46 43 45 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = ( ( 𝐹 ‘ 𝑘 ) ↾t ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) ) )
47 46 unieqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) ) )
48 40 47 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) = ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) )
49 48 ixpeq2dva ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) = X 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) )
50 ixpin ⊢ X 𝑘 ∈ 𝐴 ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ 𝑆 ) = ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∩ X 𝑘 ∈ 𝐴 𝑆 )
51 nfcv ⊢ Ⅎ 𝑦 ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 )
52 nfcv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑦 )
53 nfcv ⊢ Ⅎ 𝑘 ↾t
54 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝑆
55 52 53 54 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 )
56 55 nfuni ⊢ Ⅎ 𝑘 ∪ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 )
57 fveq2 ⊢ ( 𝑘 = 𝑦 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑦 ) )
58 csbeq1a ⊢ ( 𝑘 = 𝑦 → 𝑆 = ⦋ 𝑦 / 𝑘 ⦌ 𝑆 )
59 57 58 oveq12d ⊢ ( 𝑘 = 𝑦 → ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) )
60 59 unieqd ⊢ ( 𝑘 = 𝑦 → ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = ∪ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) )
61 51 56 60 cbvixp ⊢ X 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = X 𝑦 ∈ 𝐴 ∪ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 )
62 ixpeq2 ⊢ ( ∀ 𝑦 ∈ 𝐴 ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = ∪ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) → X 𝑦 ∈ 𝐴 ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ∪ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) )
63 ovex ⊢ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) ∈ V
64 nfcv ⊢ Ⅎ 𝑘 𝑦
65 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) )
66 64 55 59 65 fvmptf ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) ∈ V ) → ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) )
67 63 66 mpan2 ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) )
68 67 unieqd ⊢ ( 𝑦 ∈ 𝐴 → ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = ∪ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 ) )
69 62 68 mprg ⊢ X 𝑦 ∈ 𝐴 ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ∪ ( ( 𝐹 ‘ 𝑦 ) ↾t ⦋ 𝑦 / 𝑘 ⦌ 𝑆 )
70 61 69 eqtr4i ⊢ X 𝑘 ∈ 𝐴 ∪ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = X 𝑦 ∈ 𝐴 ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 )
71 49 50 70 3eqtr3g ⊢ ( 𝜑 → ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) = X 𝑦 ∈ 𝐴 ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) )
72 eqid ⊢ ( ∏t ‘ 𝐹 ) = ( ∏t ‘ 𝐹 )
73 72 ptuni ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
74 1 2 73 syl2anc ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
75 74 ineq1d ⊢ ( 𝜑 → ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) = ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) )
76 resttop ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ Top ∧ 𝑆 ∈ 𝑊 ) → ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ∈ Top )
77 36 3 76 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ∈ Top )
78 77 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) : 𝐴 ⟶ Top )
79 eqid ⊢ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) = ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) )
80 79 ptuni ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) : 𝐴 ⟶ Top ) → X 𝑦 ∈ 𝐴 ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) )
81 1 78 80 syl2anc ⊢ ( 𝜑 → X 𝑦 ∈ 𝐴 ∪ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑦 ) = ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) )
82 71 75 81 3eqtr3d ⊢ ( 𝜑 → ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) = ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) )
83 82 sneqd ⊢ ( 𝜑 → { ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) } = { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } )
84 35 83 eqtrid ⊢ ( 𝜑 → ran ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } )
85 vex ⊢ 𝑤 ∈ V
86 85 elixp ⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ↔ ( 𝑤 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑤 ‘ 𝑘 ) ∈ 𝑆 ) )
87 86 simprbi ⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 → ∀ 𝑘 ∈ 𝐴 ( 𝑤 ‘ 𝑘 ) ∈ 𝑆 )
88 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑢 / 𝑘 ⦌ 𝑆
89 88 nfel2 ⊢ Ⅎ 𝑘 ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆
90 fveq2 ⊢ ( 𝑘 = 𝑢 → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝑢 ) )
91 csbeq1a ⊢ ( 𝑘 = 𝑢 → 𝑆 = ⦋ 𝑢 / 𝑘 ⦌ 𝑆 )
92 90 91 eleq12d ⊢ ( 𝑘 = 𝑢 → ( ( 𝑤 ‘ 𝑘 ) ∈ 𝑆 ↔ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
93 89 92 rspc ⊢ ( 𝑢 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( 𝑤 ‘ 𝑘 ) ∈ 𝑆 → ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
94 87 93 syl5 ⊢ ( 𝑢 ∈ 𝐴 → ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 → ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
95 94 pm4.71d ⊢ ( 𝑢 ∈ 𝐴 → ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ↔ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ∧ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
96 95 anbi2d ⊢ ( 𝑢 ∈ 𝐴 → ( ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ∧ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
97 an4 ⊢ ( ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ∧ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ↔ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ∧ ( ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ∧ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
98 elin ⊢ ( ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ↔ ( ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ∧ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
99 98 anbi2i ⊢ ( ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ↔ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ∧ ( ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ∧ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
100 97 99 bitr4i ⊢ ( ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ∧ ( 𝑤 ‘ 𝑢 ) ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ↔ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
101 96 100 bitrdi ⊢ ( 𝑢 ∈ 𝐴 → ( ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
102 elin ⊢ ( 𝑤 ∈ ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) )
103 82 eleq2d ⊢ ( 𝜑 → ( 𝑤 ∈ ( ∪ ( ∏t ‘ 𝐹 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ) )
104 102 103 bitr3id ⊢ ( 𝜑 → ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ↔ 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ) )
105 104 anbi1d ⊢ ( 𝜑 → ( ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ↔ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
106 101 105 sylan9bbr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
107 106 abbidv ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → { 𝑤 ∣ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) } = { 𝑤 ∣ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) } )
108 eqid ⊢ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) = ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) )
109 108 mptpreima ⊢ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) = { 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 }
110 df-rab ⊢ { 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 } = { 𝑤 ∣ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) }
111 109 110 eqtr2i ⊢ { 𝑤 ∣ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) } = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 )
112 abid2 ⊢ { 𝑤 ∣ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 } = X 𝑘 ∈ 𝐴 𝑆
113 111 112 ineq12i ⊢ ( { 𝑤 ∣ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) } ∩ { 𝑤 ∣ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 } ) = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 )
114 inab ⊢ ( { 𝑤 ∣ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) } ∩ { 𝑤 ∣ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 } ) = { 𝑤 ∣ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) }
115 113 114 eqtr3i ⊢ ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) = { 𝑤 ∣ ( ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ 𝑣 ) ∧ 𝑤 ∈ X 𝑘 ∈ 𝐴 𝑆 ) }
116 eqid ⊢ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) = ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) )
117 116 mptpreima ⊢ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) = { 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ∣ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) }
118 df-rab ⊢ { 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ∣ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) } = { 𝑤 ∣ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) }
119 117 118 eqtri ⊢ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) = { 𝑤 ∣ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ∧ ( 𝑤 ‘ 𝑢 ) ∈ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) }
120 107 115 119 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
121 120 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
122 121 rexbidv ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
123 ineq1 ⊢ ( 𝑣 = 𝑦 → ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) = ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
124 123 imaeq2d ⊢ ( 𝑣 = 𝑦 → ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
125 124 eqeq2d ⊢ ( 𝑣 = 𝑦 → ( 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ↔ 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
126 125 cbvrexvw ⊢ ( ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑣 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ↔ ∃ 𝑦 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
127 122 126 bitrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑦 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
128 vex ⊢ 𝑦 ∈ V
129 128 inex1 ⊢ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ∈ V
130 129 a1i ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑢 ) ) → ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ∈ V )
131 ovex ⊢ ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ∈ V
132 nfcv ⊢ Ⅎ 𝑘 𝑢
133 nfcv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑢 )
134 133 53 88 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 )
135 fveq2 ⊢ ( 𝑘 = 𝑢 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑢 ) )
136 135 91 oveq12d ⊢ ( 𝑘 = 𝑢 → ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) = ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
137 132 134 136 65 fvmptf ⊢ ( ( 𝑢 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ∈ V ) → ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) = ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
138 131 137 mpan2 ⊢ ( 𝑢 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) = ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
139 138 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) = ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) )
140 139 eleq2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↔ 𝑣 ∈ ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
141 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑢 ∈ 𝐴 )
142 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑢 / 𝑘 ⦌ 𝑊
143 88 142 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑊
144 141 143 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑊 )
145 eleq1w ⊢ ( 𝑘 = 𝑢 → ( 𝑘 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴 ) )
146 145 anbi2d ⊢ ( 𝑘 = 𝑢 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ) )
147 csbeq1a ⊢ ( 𝑘 = 𝑢 → 𝑊 = ⦋ 𝑢 / 𝑘 ⦌ 𝑊 )
148 91 147 eleq12d ⊢ ( 𝑘 = 𝑢 → ( 𝑆 ∈ 𝑊 ↔ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑊 ) )
149 146 148 imbi12d ⊢ ( 𝑘 = 𝑢 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑊 ) ) )
150 144 149 3 chvarfv ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑊 )
151 elrest ⊢ ( ( ( 𝐹 ‘ 𝑢 ) ∈ V ∧ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ∈ ⦋ 𝑢 / 𝑘 ⦌ 𝑊 ) → ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ↔ ∃ 𝑦 ∈ ( 𝐹 ‘ 𝑢 ) 𝑣 = ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
152 6 150 151 sylancr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑢 ) ↾t ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ↔ ∃ 𝑦 ∈ ( 𝐹 ‘ 𝑢 ) 𝑣 = ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
153 140 152 bitrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↔ ∃ 𝑦 ∈ ( 𝐹 ‘ 𝑢 ) 𝑣 = ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
154 imaeq2 ⊢ ( 𝑣 = ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) → ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) )
155 154 eqeq2d ⊢ ( 𝑣 = ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) → ( 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ↔ 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
156 155 adantl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 = ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) → ( 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ↔ 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
157 130 153 156 rexxfr2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ↔ ∃ 𝑦 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ ( 𝑦 ∩ ⦋ 𝑢 / 𝑘 ⦌ 𝑆 ) ) ) )
158 127 157 bitr4d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) )
159 158 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) )
160 159 abbidv ⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) } = { 𝑥 ∣ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) } )
161 eqid ⊢ ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) )
162 161 rnmpt ⊢ ran ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) 𝑦 = ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) }
163 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) 𝑦 = ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 )
164 nfv ⊢ Ⅎ 𝑦 ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 )
165 28 mptex ⊢ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) ∈ V
166 165 cnvex ⊢ ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) ∈ V
167 166 imaex ⊢ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∈ V
168 167 rgen2w ⊢ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∈ V
169 ineq1 ⊢ ( 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) → ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) )
170 169 eqeq2d ⊢ ( 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) → ( 𝑦 = ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ 𝑦 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
171 8 170 rexrnmpo ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∈ V → ( ∃ 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) 𝑦 = ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑦 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
172 168 171 ax-mp ⊢ ( ∃ 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) 𝑦 = ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑦 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) )
173 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
174 173 2rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑦 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
175 172 174 bitrid ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) 𝑦 = ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) )
176 163 164 175 cbvabw ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) 𝑦 = ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) } = { 𝑥 ∣ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) }
177 162 176 eqtri ⊢ ran ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = { 𝑥 ∣ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) 𝑥 = ( ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ∩ X 𝑘 ∈ 𝐴 𝑆 ) }
178 eqid ⊢ ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) )
179 178 rnmpo ⊢ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) = { 𝑥 ∣ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) 𝑥 = ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) }
180 160 177 179 3eqtr4g ⊢ ( 𝜑 → ran ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) )
181 84 180 uneq12d ⊢ ( 𝜑 → ( ran ( 𝑥 ∈ { ∪ ( ∏t ‘ 𝐹 ) } ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ∪ ran ( 𝑥 ∈ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) ) = ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) )
182 23 181 eqtrid ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↦ ( 𝑥 ∩ X 𝑘 ∈ 𝐴 𝑆 ) ) = ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) )
183 19 182 eqtrd ⊢ ( 𝜑 → ( ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) )
184 183 fveq2d ⊢ ( 𝜑 → ( fi ‘ ( ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) ) = ( fi ‘ ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) )
185 4 184 eqtr3id ⊢ ( 𝜑 → ( ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ( fi ‘ ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) )
186 185 fveq2d ⊢ ( 𝜑 → ( topGen ‘ ( ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) ) = ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) )
187 eqid ⊢ ∪ ( ∏t ‘ 𝐹 ) = ∪ ( ∏t ‘ 𝐹 )
188 72 187 8 ptval2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) )
189 1 2 188 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) = ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) )
190 189 oveq1d ⊢ ( 𝜑 → ( ( ∏t ‘ 𝐹 ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ( ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) )
191 fvex ⊢ ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ∈ V
192 tgrest ⊢ ( ( ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ∈ V ∧ X 𝑘 ∈ 𝐴 𝑆 ∈ V ) → ( topGen ‘ ( ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) ) = ( ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) )
193 191 17 192 sylancr ⊢ ( 𝜑 → ( topGen ‘ ( ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) ) = ( ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) )
194 190 193 eqtr4d ⊢ ( 𝜑 → ( ( ∏t ‘ 𝐹 ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ( topGen ‘ ( ( fi ‘ ( { ∪ ( ∏t ‘ 𝐹 ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) ) )
195 eqid ⊢ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) = ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) )
196 79 195 178 ptval2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) : 𝐴 ⟶ Top ) → ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) = ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) )
197 1 78 196 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) = ( topGen ‘ ( fi ‘ ( { ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) } ∪ ran ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ( ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ‘ 𝑢 ) ↦ ( ◡ ( 𝑤 ∈ ∪ ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) ↦ ( 𝑤 ‘ 𝑢 ) ) “ 𝑣 ) ) ) ) ) )
198 186 194 197 3eqtr4d ⊢ ( 𝜑 → ( ( ∏t ‘ 𝐹 ) ↾t X 𝑘 ∈ 𝐴 𝑆 ) = ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ↾t 𝑆 ) ) ) )