Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ptrest Structured version   Visualization version   GIF version
Theorem ptrest 36476
Description: Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.)
Hypotheses
Ref Expression
ptrest.0 (πœ‘ β†’ 𝐴 ∈ 𝑉)
ptrest.1 (πœ‘ β†’ 𝐹:𝐴⟢Top)
ptrest.2 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 ∈ π‘Š)
Assertion
Ref Expression
ptrest (πœ‘ β†’ ((∏tβ€˜πΉ) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
Distinct variable groups:   πœ‘,π‘˜   𝐴,π‘˜   π‘˜,𝐹   π‘˜,𝑉
Allowed substitution hints:   𝑆(π‘˜)   π‘Š(π‘˜)
Proof of Theorem ptrest
Dummy variables 𝑒 𝑣 𝑀 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 firest 17375 . . . 4 (fiβ€˜(({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = ((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)
2 snex 5431 . . . . . . . 8 {βˆͺ (∏tβ€˜πΉ)} ∈ V
3 ptrest.0 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ 𝑉)
4 fvex 6902 . . . . . . . . . . 11 (πΉβ€˜π‘’) ∈ V
54rgenw 3066 . . . . . . . . . 10 βˆ€π‘’ ∈ 𝐴 (πΉβ€˜π‘’) ∈ V
6 eqid 2733 . . . . . . . . . . 11 (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) = (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))
76mpoexxg 8059 . . . . . . . . . 10 ((𝐴 ∈ 𝑉 ∧ βˆ€π‘’ ∈ 𝐴 (πΉβ€˜π‘’) ∈ V) β†’ (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
83, 5, 7sylancl 587 . . . . . . . . 9 (πœ‘ β†’ (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
9 rnexg 7892 . . . . . . . . 9 ((𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V β†’ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
108, 9syl 17 . . . . . . . 8 (πœ‘ β†’ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
11 unexg 7733 . . . . . . . 8 (({βˆͺ (∏tβ€˜πΉ)} ∈ V ∧ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V) β†’ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ∈ V)
122, 10, 11sylancr 588 . . . . . . 7 (πœ‘ β†’ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ∈ V)
13 ptrest.2 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 ∈ π‘Š)
1413ralrimiva 3147 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝑆 ∈ π‘Š)
15 ixpexg 8913 . . . . . . . 8 (βˆ€π‘˜ ∈ 𝐴 𝑆 ∈ π‘Š β†’ Xπ‘˜ ∈ 𝐴 𝑆 ∈ V)
1614, 15syl 17 . . . . . . 7 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 𝑆 ∈ V)
17 restval 17369 . . . . . . 7 ((({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ∈ V ∧ Xπ‘˜ ∈ 𝐴 𝑆 ∈ V) β†’ (({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
1812, 16, 17syl2anc 585 . . . . . 6 (πœ‘ β†’ (({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
19 mptun 6694 . . . . . . . . 9 (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ((π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
2019rneqi 5935 . . . . . . . 8 ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ran ((π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
21 rnun 6143 . . . . . . . 8 ran ((π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆))) = (ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
2220, 21eqtri 2761 . . . . . . 7 ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = (ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
23 elsni 4645 . . . . . . . . . . . . . 14 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} β†’ π‘₯ = βˆͺ (∏tβ€˜πΉ))
2423ineq1d 4211 . . . . . . . . . . . . 13 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} β†’ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) = (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
2524mpteq2ia 5251 . . . . . . . . . . . 12 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
26 fvex 6902 . . . . . . . . . . . . . 14 (∏tβ€˜πΉ) ∈ V
2726uniex 7728 . . . . . . . . . . . . 13 βˆͺ (∏tβ€˜πΉ) ∈ V
2827inex1 5317 . . . . . . . . . . . . 13 (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ∈ V
29 fmptsn 7162 . . . . . . . . . . . . 13 ((βˆͺ (∏tβ€˜πΉ) ∈ V ∧ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ∈ V) β†’ {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩} = (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
3027, 28, 29mp2an 691 . . . . . . . . . . . 12 {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩} = (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
3125, 30eqtr4i 2764 . . . . . . . . . . 11 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩}
3231rneqi 5935 . . . . . . . . . 10 ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ran {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩}
3327rnsnop 6221 . . . . . . . . . 10 ran {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩} = {(βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
3432, 33eqtri 2761 . . . . . . . . 9 ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {(βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
35 ptrest.1 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:𝐴⟢Top)
3635ffvelcdmda 7084 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ (πΉβ€˜π‘˜) ∈ Top)
37 inss1 4228 . . . . . . . . . . . . . . 15 (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) βŠ† βˆͺ (πΉβ€˜π‘˜)
38 eqid 2733 . . . . . . . . . . . . . . . 16 βˆͺ (πΉβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜)
3938restuni 22658 . . . . . . . . . . . . . . 15 (((πΉβ€˜π‘˜) ∈ Top ∧ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) βŠ† βˆͺ (πΉβ€˜π‘˜)) β†’ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
4036, 37, 39sylancl 587 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
41 fvex 6902 . . . . . . . . . . . . . . . . 17 (πΉβ€˜π‘˜) ∈ V
4238restin 22662 . . . . . . . . . . . . . . . . 17 (((πΉβ€˜π‘˜) ∈ V ∧ 𝑆 ∈ π‘Š) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘˜) β†Ύt (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜))))
4341, 13, 42sylancr 588 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘˜) β†Ύt (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜))))
44 incom 4201 . . . . . . . . . . . . . . . . 17 (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜)) = (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)
4544oveq2i 7417 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘˜) β†Ύt (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜))) = ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆))
4643, 45eqtrdi 2789 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
4746unieqd 4922 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
4840, 47eqtr4d 2776 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆))
4948ixpeq2dva 8903 . . . . . . . . . . . 12 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = Xπ‘˜ ∈ 𝐴 βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆))
50 ixpin 8914 . . . . . . . . . . . 12 Xπ‘˜ ∈ 𝐴 (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = (Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) ∩ Xπ‘˜ ∈ 𝐴 𝑆)
51 nfcv 2904 . . . . . . . . . . . . . 14 Ⅎ𝑦βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆)
52 nfcv 2904 . . . . . . . . . . . . . . . 16 β„²π‘˜(πΉβ€˜π‘¦)
53 nfcv 2904 . . . . . . . . . . . . . . . 16 β„²π‘˜ β†Ύt
54 nfcsb1v 3918 . . . . . . . . . . . . . . . 16 β„²π‘˜β¦‹π‘¦ / π‘˜β¦Œπ‘†
5552, 53, 54nfov 7436 . . . . . . . . . . . . . . 15 β„²π‘˜((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
5655nfuni 4915 . . . . . . . . . . . . . 14 β„²π‘˜βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
57 fveq2 6889 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑦 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘¦))
58 csbeq1a 3907 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑦 β†’ 𝑆 = ⦋𝑦 / π‘˜β¦Œπ‘†)
5957, 58oveq12d 7424 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑦 β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6059unieqd 4922 . . . . . . . . . . . . . 14 (π‘˜ = 𝑦 β†’ βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6151, 56, 60cbvixp 8905 . . . . . . . . . . . . 13 Xπ‘˜ ∈ 𝐴 βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = X𝑦 ∈ 𝐴 βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
62 ixpeq2 8902 . . . . . . . . . . . . . 14 (βˆ€π‘¦ ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†) β†’ X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = X𝑦 ∈ 𝐴 βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
63 ovex 7439 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†) ∈ V
64 nfcv 2904 . . . . . . . . . . . . . . . . 17 β„²π‘˜π‘¦
65 eqid 2733 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)) = (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))
6664, 55, 59, 65fvmptf 7017 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝐴 ∧ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†) ∈ V) β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6763, 66mpan2 690 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝐴 β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6867unieqd 4922 . . . . . . . . . . . . . 14 (𝑦 ∈ 𝐴 β†’ βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6962, 68mprg 3068 . . . . . . . . . . . . 13 X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = X𝑦 ∈ 𝐴 βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
7061, 69eqtr4i 2764 . . . . . . . . . . . 12 Xπ‘˜ ∈ 𝐴 βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦)
7149, 50, 703eqtr3g 2796 . . . . . . . . . . 11 (πœ‘ β†’ (Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦))
72 eqid 2733 . . . . . . . . . . . . . 14 (∏tβ€˜πΉ) = (∏tβ€˜πΉ)
7372ptuni 23090 . . . . . . . . . . . . 13 ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟢Top) β†’ Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) = βˆͺ (∏tβ€˜πΉ))
743, 35, 73syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) = βˆͺ (∏tβ€˜πΉ))
7574ineq1d 4211 . . . . . . . . . . 11 (πœ‘ β†’ (Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
76 resttop 22656 . . . . . . . . . . . . . 14 (((πΉβ€˜π‘˜) ∈ Top ∧ 𝑆 ∈ π‘Š) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) ∈ Top)
7736, 13, 76syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) ∈ Top)
7877fmpttd 7112 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)):𝐴⟢Top)
79 eqid 2733 . . . . . . . . . . . . 13 (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))
8079ptuni 23090 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)):𝐴⟢Top) β†’ X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
813, 78, 80syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
8271, 75, 813eqtr3d 2781 . . . . . . . . . 10 (πœ‘ β†’ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
8382sneqd 4640 . . . . . . . . 9 (πœ‘ β†’ {(βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)} = {βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))})
8434, 83eqtrid 2785 . . . . . . . 8 (πœ‘ β†’ ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))})
85 vex 3479 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑀 ∈ V
8685elixp 8895 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ↔ (𝑀 Fn 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 (π‘€β€˜π‘˜) ∈ 𝑆))
8786simprbi 498 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 β†’ βˆ€π‘˜ ∈ 𝐴 (π‘€β€˜π‘˜) ∈ 𝑆)
88 nfcsb1v 3918 . . . . . . . . . . . . . . . . . . . . . . . 24 β„²π‘˜β¦‹π‘’ / π‘˜β¦Œπ‘†
8988nfel2 2922 . . . . . . . . . . . . . . . . . . . . . . 23 β„²π‘˜(π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†
90 fveq2 6889 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑒 β†’ (π‘€β€˜π‘˜) = (π‘€β€˜π‘’))
91 csbeq1a 3907 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑒 β†’ 𝑆 = ⦋𝑒 / π‘˜β¦Œπ‘†)
9290, 91eleq12d 2828 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝑒 β†’ ((π‘€β€˜π‘˜) ∈ 𝑆 ↔ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9389, 92rspc 3601 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 (π‘€β€˜π‘˜) ∈ 𝑆 β†’ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9487, 93syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ 𝐴 β†’ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 β†’ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9594pm4.71d 563 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ 𝐴 β†’ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ↔ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)))
9695anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (𝑒 ∈ 𝐴 β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))))
97 an4 655 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ ((π‘€β€˜π‘’) ∈ 𝑣 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)))
98 elin 3964 . . . . . . . . . . . . . . . . . . . . 21 ((π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) ↔ ((π‘€β€˜π‘’) ∈ 𝑣 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9998anbi2i 624 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ ((π‘€β€˜π‘’) ∈ 𝑣 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)))
10097, 99bitr4i 278 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
10196, 100bitrdi 287 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ 𝐴 β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
102 elin 3964 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆))
10382eleq2d 2820 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝑀 ∈ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ 𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))))
104102, 103bitr3id 285 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ 𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))))
105104anbi1d 631 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
106101, 105sylan9bbr 512 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
107106abbidv 2802 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ {𝑀 ∣ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆)} = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))})
108 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) = (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’))
109108mptpreima 6235 . . . . . . . . . . . . . . . . . . 19 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) = {𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∣ (π‘€β€˜π‘’) ∈ 𝑣}
110 df-rab 3434 . . . . . . . . . . . . . . . . . . 19 {𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∣ (π‘€β€˜π‘’) ∈ 𝑣} = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)}
111109, 110eqtr2i 2762 . . . . . . . . . . . . . . . . . 18 {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)} = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)
112 abid2 2872 . . . . . . . . . . . . . . . . . 18 {𝑀 ∣ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆} = Xπ‘˜ ∈ 𝐴 𝑆
113111, 112ineq12i 4210 . . . . . . . . . . . . . . . . 17 ({𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)} ∩ {𝑀 ∣ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆}) = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)
114 inab 4299 . . . . . . . . . . . . . . . . 17 ({𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)} ∩ {𝑀 ∣ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆}) = {𝑀 ∣ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆)}
115113, 114eqtr3i 2763 . . . . . . . . . . . . . . . 16 ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = {𝑀 ∣ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆)}
116 eqid 2733 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) = (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’))
117116mptpreima 6235 . . . . . . . . . . . . . . . . 17 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) = {𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∣ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)}
118 df-rab 3434 . . . . . . . . . . . . . . . . 17 {𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∣ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)} = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))}
119117, 118eqtri 2761 . . . . . . . . . . . . . . . 16 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))}
120107, 115, 1193eqtr4g 2798 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
121120eqeq2d 2744 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
122121rexbidv 3179 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
123 ineq1 4205 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑦 β†’ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))
124123imaeq2d 6058 . . . . . . . . . . . . . . 15 (𝑣 = 𝑦 β†’ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
125124eqeq2d 2744 . . . . . . . . . . . . . 14 (𝑣 = 𝑦 β†’ (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
126125cbvrexvw 3236 . . . . . . . . . . . . 13 (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
127122, 126bitrdi 287 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
128 vex 3479 . . . . . . . . . . . . . . 15 𝑦 ∈ V
129128inex1 5317 . . . . . . . . . . . . . 14 (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V
130129a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐴) ∧ 𝑦 ∈ (πΉβ€˜π‘’)) β†’ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V)
131 ovex 7439 . . . . . . . . . . . . . . . . 17 ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V
132 nfcv 2904 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘’
133 nfcv 2904 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜(πΉβ€˜π‘’)
134133, 53, 88nfov 7436 . . . . . . . . . . . . . . . . . 18 β„²π‘˜((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†)
135 fveq2 6889 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑒 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘’))
136135, 91oveq12d 7424 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
137132, 134, 136, 65fvmptf 7017 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ 𝐴 ∧ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V) β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
138131, 137mpan2 690 . . . . . . . . . . . . . . . 16 (𝑒 ∈ 𝐴 β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
139138adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
140139eleq2d 2820 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↔ 𝑣 ∈ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†)))
141 nfv 1918 . . . . . . . . . . . . . . . . 17 β„²π‘˜(πœ‘ ∧ 𝑒 ∈ 𝐴)
142 nfcsb1v 3918 . . . . . . . . . . . . . . . . . 18 β„²π‘˜β¦‹π‘’ / π‘˜β¦Œπ‘Š
14388, 142nfel 2918 . . . . . . . . . . . . . . . . 17 β„²π‘˜β¦‹π‘’ / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š
144141, 143nfim 1900 . . . . . . . . . . . . . . . 16 β„²π‘˜((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š)
145 eleq1w 2817 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ (π‘˜ ∈ 𝐴 ↔ 𝑒 ∈ 𝐴))
146145anbi2d 630 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑒 β†’ ((πœ‘ ∧ π‘˜ ∈ 𝐴) ↔ (πœ‘ ∧ 𝑒 ∈ 𝐴)))
147 csbeq1a 3907 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ π‘Š = ⦋𝑒 / π‘˜β¦Œπ‘Š)
14891, 147eleq12d 2828 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑒 β†’ (𝑆 ∈ π‘Š ↔ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š))
149146, 148imbi12d 345 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑒 β†’ (((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 ∈ π‘Š) ↔ ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š)))
150144, 149, 13chvarfv 2234 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š)
151 elrest 17370 . . . . . . . . . . . . . . 15 (((πΉβ€˜π‘’) ∈ V ∧ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š) β†’ (𝑣 ∈ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
1524, 150, 151sylancr 588 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
153140, 152bitrd 279 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
154 imaeq2 6054 . . . . . . . . . . . . . . 15 (𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) β†’ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
155154eqeq2d 2744 . . . . . . . . . . . . . 14 (𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) β†’ (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
156155adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) β†’ (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
157130, 153, 156rexxfr2d 5409 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
158127, 157bitr4d 282 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))
159158rexbidva 3177 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))
160159abbidv 2802 . . . . . . . . 9 (πœ‘ β†’ {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)} = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)})
161 eqid 2733 . . . . . . . . . . 11 (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆))
162161rnmpt 5953 . . . . . . . . . 10 ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {𝑦 ∣ βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
163 nfre1 3283 . . . . . . . . . . 11 β„²π‘₯βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)
164 nfv 1918 . . . . . . . . . . 11 β„²π‘¦βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)
16527mptex 7222 . . . . . . . . . . . . . . . 16 (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) ∈ V
166165cnvex 7913 . . . . . . . . . . . . . . 15 β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) ∈ V
167166imaex 7904 . . . . . . . . . . . . . 14 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∈ V
168167rgen2w 3067 . . . . . . . . . . . . 13 βˆ€π‘’ ∈ 𝐴 βˆ€π‘£ ∈ (πΉβ€˜π‘’)(β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∈ V
169 ineq1 4205 . . . . . . . . . . . . . . 15 (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) β†’ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
170169eqeq2d 2744 . . . . . . . . . . . . . 14 (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) β†’ (𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ 𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
1716, 170rexrnmpo 7545 . . . . . . . . . . . . 13 (βˆ€π‘’ ∈ 𝐴 βˆ€π‘£ ∈ (πΉβ€˜π‘’)(β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∈ V β†’ (βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
172168, 171ax-mp 5 . . . . . . . . . . . 12 (βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
173 eqeq1 2737 . . . . . . . . . . . . 13 (𝑦 = π‘₯ β†’ (𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
1741732rexbidv 3220 . . . . . . . . . . . 12 (𝑦 = π‘₯ β†’ (βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
175172, 174bitrid 283 . . . . . . . . . . 11 (𝑦 = π‘₯ β†’ (βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
176163, 164, 175cbvabw 2807 . . . . . . . . . 10 {𝑦 ∣ βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)} = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
177162, 176eqtri 2761 . . . . . . . . 9 ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
178 eqid 2733 . . . . . . . . . 10 (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) = (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))
179178rnmpo 7539 . . . . . . . . 9 ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)}
180160, 177, 1793eqtr4g 2798 . . . . . . . 8 (πœ‘ β†’ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))
18184, 180uneq12d 4164 . . . . . . 7 (πœ‘ β†’ (ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆))) = ({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))
18222, 181eqtrid 2785 . . . . . 6 (πœ‘ β†’ ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))
18318, 182eqtrd 2773 . . . . 5 (πœ‘ β†’ (({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))
184183fveq2d 6893 . . . 4 (πœ‘ β†’ (fiβ€˜(({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = (fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))))
1851, 184eqtr3id 2787 . . 3 (πœ‘ β†’ ((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = (fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))))
186185fveq2d 6893 . 2 (πœ‘ β†’ (topGenβ€˜((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
187 eqid 2733 . . . . . 6 βˆͺ (∏tβ€˜πΉ) = βˆͺ (∏tβ€˜πΉ)
18872, 187, 6ptval2 23097 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟢Top) β†’ (∏tβ€˜πΉ) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
1893, 35, 188syl2anc 585 . . . 4 (πœ‘ β†’ (∏tβ€˜πΉ) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
190189oveq1d 7421 . . 3 (πœ‘ β†’ ((∏tβ€˜πΉ) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ((topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆))
191 fvex 6902 . . . 4 (fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) ∈ V
192 tgrest 22655 . . . 4 (((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) ∈ V ∧ Xπ‘˜ ∈ 𝐴 𝑆 ∈ V) β†’ (topGenβ€˜((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = ((topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆))
193191, 16, 192sylancr 588 . . 3 (πœ‘ β†’ (topGenβ€˜((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = ((topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆))
194190, 193eqtr4d 2776 . 2 (πœ‘ β†’ ((∏tβ€˜πΉ) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = (topGenβ€˜((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)))
195 eqid 2733 . . . 4 βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))
19679, 195, 178ptval2 23097 . . 3 ((𝐴 ∈ 𝑉 ∧ (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)):𝐴⟢Top) β†’ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
1973, 78, 196syl2anc 585 . 2 (πœ‘ β†’ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
198186, 194, 1973eqtr4d 2783 1 (πœ‘ β†’ ((∏tβ€˜πΉ) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475  β¦‹csb 3893   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  {csn 4628  βŸ¨cop 4634  βˆͺ cuni 4908   ↦ cmpt 5231  β—‘ccnv 5675  ran crn 5677   β€œ cima 5679   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ∈ cmpo 7408  Xcixp 8888  ficfi 9402   β†Ύt crest 17363  topGenctg 17380  βˆtcpt 17381  Topctop 22387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-1o 8463  df-er 8700  df-ixp 8889  df-en 8937  df-dom 8938  df-fin 8940  df-fi 9403  df-rest 17365  df-topgen 17386  df-pt 17387  df-top 22388  df-topon 22405  df-bases 22441
This theorem is referenced by:  poimirlem30  36507
  Copyright terms: Public domain W3C validator