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 36790
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 17382 . . . 4 (fiβ€˜(({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = ((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)
2 snex 5430 . . . . . . . 8 {βˆͺ (∏tβ€˜πΉ)} ∈ V
3 ptrest.0 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ 𝑉)
4 fvex 6903 . . . . . . . . . . 11 (πΉβ€˜π‘’) ∈ V
54rgenw 3063 . . . . . . . . . 10 βˆ€π‘’ ∈ 𝐴 (πΉβ€˜π‘’) ∈ V
6 eqid 2730 . . . . . . . . . . 11 (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) = (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))
76mpoexxg 8064 . . . . . . . . . 10 ((𝐴 ∈ 𝑉 ∧ βˆ€π‘’ ∈ 𝐴 (πΉβ€˜π‘’) ∈ V) β†’ (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
83, 5, 7sylancl 584 . . . . . . . . 9 (πœ‘ β†’ (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
9 rnexg 7897 . . . . . . . . 9 ((𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V β†’ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
108, 9syl 17 . . . . . . . 8 (πœ‘ β†’ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V)
11 unexg 7738 . . . . . . . 8 (({βˆͺ (∏tβ€˜πΉ)} ∈ V ∧ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ∈ V) β†’ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ∈ V)
122, 10, 11sylancr 585 . . . . . . 7 (πœ‘ β†’ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ∈ V)
13 ptrest.2 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 ∈ π‘Š)
1413ralrimiva 3144 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝑆 ∈ π‘Š)
15 ixpexg 8918 . . . . . . . 8 (βˆ€π‘˜ ∈ 𝐴 𝑆 ∈ π‘Š β†’ Xπ‘˜ ∈ 𝐴 𝑆 ∈ V)
1614, 15syl 17 . . . . . . 7 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 𝑆 ∈ V)
17 restval 17376 . . . . . . 7 ((({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ∈ V ∧ Xπ‘˜ ∈ 𝐴 𝑆 ∈ V) β†’ (({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
1812, 16, 17syl2anc 582 . . . . . 6 (πœ‘ β†’ (({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
19 mptun 6695 . . . . . . . . 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 6144 . . . . . . . 8 ran ((π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆))) = (ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
2220, 21eqtri 2758 . . . . . . 7 ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = (ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
23 elsni 4644 . . . . . . . . . . . . . 14 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} β†’ π‘₯ = βˆͺ (∏tβ€˜πΉ))
2423ineq1d 4210 . . . . . . . . . . . . 13 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} β†’ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) = (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
2524mpteq2ia 5250 . . . . . . . . . . . 12 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
26 fvex 6903 . . . . . . . . . . . . . 14 (∏tβ€˜πΉ) ∈ V
2726uniex 7733 . . . . . . . . . . . . 13 βˆͺ (∏tβ€˜πΉ) ∈ V
2827inex1 5316 . . . . . . . . . . . . 13 (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ∈ V
29 fmptsn 7166 . . . . . . . . . . . . 13 ((βˆͺ (∏tβ€˜πΉ) ∈ V ∧ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ∈ V) β†’ {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩} = (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
3027, 28, 29mp2an 688 . . . . . . . . . . . 12 {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩} = (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
3125, 30eqtr4i 2761 . . . . . . . . . . 11 (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩}
3231rneqi 5935 . . . . . . . . . 10 ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ran {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩}
3327rnsnop 6222 . . . . . . . . . 10 ran {⟨βˆͺ (∏tβ€˜πΉ), (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)⟩} = {(βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
3432, 33eqtri 2758 . . . . . . . . 9 ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {(βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
35 ptrest.1 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:𝐴⟢Top)
3635ffvelcdmda 7085 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ (πΉβ€˜π‘˜) ∈ Top)
37 inss1 4227 . . . . . . . . . . . . . . 15 (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) βŠ† βˆͺ (πΉβ€˜π‘˜)
38 eqid 2730 . . . . . . . . . . . . . . . 16 βˆͺ (πΉβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜)
3938restuni 22886 . . . . . . . . . . . . . . 15 (((πΉβ€˜π‘˜) ∈ Top ∧ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) βŠ† βˆͺ (πΉβ€˜π‘˜)) β†’ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
4036, 37, 39sylancl 584 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
41 fvex 6903 . . . . . . . . . . . . . . . . 17 (πΉβ€˜π‘˜) ∈ V
4238restin 22890 . . . . . . . . . . . . . . . . 17 (((πΉβ€˜π‘˜) ∈ V ∧ 𝑆 ∈ π‘Š) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘˜) β†Ύt (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜))))
4341, 13, 42sylancr 585 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘˜) β†Ύt (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜))))
44 incom 4200 . . . . . . . . . . . . . . . . 17 (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜)) = (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)
4544oveq2i 7422 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘˜) β†Ύt (𝑆 ∩ βˆͺ (πΉβ€˜π‘˜))) = ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆))
4643, 45eqtrdi 2786 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
4746unieqd 4921 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆)))
4840, 47eqtr4d 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆))
4948ixpeq2dva 8908 . . . . . . . . . . . 12 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = Xπ‘˜ ∈ 𝐴 βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆))
50 ixpin 8919 . . . . . . . . . . . 12 Xπ‘˜ ∈ 𝐴 (βˆͺ (πΉβ€˜π‘˜) ∩ 𝑆) = (Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) ∩ Xπ‘˜ ∈ 𝐴 𝑆)
51 nfcv 2901 . . . . . . . . . . . . . 14 Ⅎ𝑦βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆)
52 nfcv 2901 . . . . . . . . . . . . . . . 16 β„²π‘˜(πΉβ€˜π‘¦)
53 nfcv 2901 . . . . . . . . . . . . . . . 16 β„²π‘˜ β†Ύt
54 nfcsb1v 3917 . . . . . . . . . . . . . . . 16 β„²π‘˜β¦‹π‘¦ / π‘˜β¦Œπ‘†
5552, 53, 54nfov 7441 . . . . . . . . . . . . . . 15 β„²π‘˜((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
5655nfuni 4914 . . . . . . . . . . . . . 14 β„²π‘˜βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
57 fveq2 6890 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑦 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘¦))
58 csbeq1a 3906 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑦 β†’ 𝑆 = ⦋𝑦 / π‘˜β¦Œπ‘†)
5957, 58oveq12d 7429 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑦 β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6059unieqd 4921 . . . . . . . . . . . . . 14 (π‘˜ = 𝑦 β†’ βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6151, 56, 60cbvixp 8910 . . . . . . . . . . . . 13 Xπ‘˜ ∈ 𝐴 βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = X𝑦 ∈ 𝐴 βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
62 ixpeq2 8907 . . . . . . . . . . . . . 14 (βˆ€π‘¦ ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†) β†’ X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = X𝑦 ∈ 𝐴 βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
63 ovex 7444 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†) ∈ V
64 nfcv 2901 . . . . . . . . . . . . . . . . 17 β„²π‘˜π‘¦
65 eqid 2730 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)) = (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))
6664, 55, 59, 65fvmptf 7018 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝐴 ∧ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†) ∈ V) β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6763, 66mpan2 687 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝐴 β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6867unieqd 4921 . . . . . . . . . . . . . 14 (𝑦 ∈ 𝐴 β†’ βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†))
6962, 68mprg 3065 . . . . . . . . . . . . 13 X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = X𝑦 ∈ 𝐴 βˆͺ ((πΉβ€˜π‘¦) β†Ύt ⦋𝑦 / π‘˜β¦Œπ‘†)
7061, 69eqtr4i 2761 . . . . . . . . . . . 12 Xπ‘˜ ∈ 𝐴 βˆͺ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦)
7149, 50, 703eqtr3g 2793 . . . . . . . . . . 11 (πœ‘ β†’ (Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦))
72 eqid 2730 . . . . . . . . . . . . . 14 (∏tβ€˜πΉ) = (∏tβ€˜πΉ)
7372ptuni 23318 . . . . . . . . . . . . 13 ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟢Top) β†’ Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) = βˆͺ (∏tβ€˜πΉ))
743, 35, 73syl2anc 582 . . . . . . . . . . . 12 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) = βˆͺ (∏tβ€˜πΉ))
7574ineq1d 4210 . . . . . . . . . . 11 (πœ‘ β†’ (Xπ‘˜ ∈ 𝐴 βˆͺ (πΉβ€˜π‘˜) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
76 resttop 22884 . . . . . . . . . . . . . 14 (((πΉβ€˜π‘˜) ∈ Top ∧ 𝑆 ∈ π‘Š) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) ∈ Top)
7736, 13, 76syl2anc 582 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) ∈ Top)
7877fmpttd 7115 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)):𝐴⟢Top)
79 eqid 2730 . . . . . . . . . . . . 13 (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))
8079ptuni 23318 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)):𝐴⟢Top) β†’ X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
813, 78, 80syl2anc 582 . . . . . . . . . . 11 (πœ‘ β†’ X𝑦 ∈ 𝐴 βˆͺ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘¦) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
8271, 75, 813eqtr3d 2778 . . . . . . . . . 10 (πœ‘ β†’ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
8382sneqd 4639 . . . . . . . . 9 (πœ‘ β†’ {(βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆)} = {βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))})
8434, 83eqtrid 2782 . . . . . . . 8 (πœ‘ β†’ ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))})
85 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑀 ∈ V
8685elixp 8900 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ↔ (𝑀 Fn 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 (π‘€β€˜π‘˜) ∈ 𝑆))
8786simprbi 495 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 β†’ βˆ€π‘˜ ∈ 𝐴 (π‘€β€˜π‘˜) ∈ 𝑆)
88 nfcsb1v 3917 . . . . . . . . . . . . . . . . . . . . . . . 24 β„²π‘˜β¦‹π‘’ / π‘˜β¦Œπ‘†
8988nfel2 2919 . . . . . . . . . . . . . . . . . . . . . . 23 β„²π‘˜(π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†
90 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑒 β†’ (π‘€β€˜π‘˜) = (π‘€β€˜π‘’))
91 csbeq1a 3906 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑒 β†’ 𝑆 = ⦋𝑒 / π‘˜β¦Œπ‘†)
9290, 91eleq12d 2825 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝑒 β†’ ((π‘€β€˜π‘˜) ∈ 𝑆 ↔ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9389, 92rspc 3599 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 (π‘€β€˜π‘˜) ∈ 𝑆 β†’ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9487, 93syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ 𝐴 β†’ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 β†’ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9594pm4.71d 560 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ 𝐴 β†’ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ↔ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)))
9695anbi2d 627 . . . . . . . . . . . . . . . . . . 19 (𝑒 ∈ 𝐴 β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))))
97 an4 652 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ ((π‘€β€˜π‘’) ∈ 𝑣 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)))
98 elin 3963 . . . . . . . . . . . . . . . . . . . . 21 ((π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) ↔ ((π‘€β€˜π‘’) ∈ 𝑣 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†))
9998anbi2i 621 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ ((π‘€β€˜π‘’) ∈ 𝑣 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)))
10097, 99bitr4i 277 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ (𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆 ∧ (π‘€β€˜π‘’) ∈ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
10196, 100bitrdi 286 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ 𝐴 β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
102 elin 3963 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆))
10382eleq2d 2817 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝑀 ∈ (βˆͺ (∏tβ€˜πΉ) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ 𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))))
104102, 103bitr3id 284 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ 𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))))
105104anbi1d 628 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
106101, 105sylan9bbr 509 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆) ↔ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
107106abbidv 2799 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ {𝑀 ∣ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆)} = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))})
108 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) = (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’))
109108mptpreima 6236 . . . . . . . . . . . . . . . . . . 19 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) = {𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∣ (π‘€β€˜π‘’) ∈ 𝑣}
110 df-rab 3431 . . . . . . . . . . . . . . . . . . 19 {𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∣ (π‘€β€˜π‘’) ∈ 𝑣} = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)}
111109, 110eqtr2i 2759 . . . . . . . . . . . . . . . . . 18 {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)} = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)
112 abid2 2869 . . . . . . . . . . . . . . . . . 18 {𝑀 ∣ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆} = Xπ‘˜ ∈ 𝐴 𝑆
113111, 112ineq12i 4209 . . . . . . . . . . . . . . . . 17 ({𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)} ∩ {𝑀 ∣ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆}) = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)
114 inab 4298 . . . . . . . . . . . . . . . . 17 ({𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣)} ∩ {𝑀 ∣ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆}) = {𝑀 ∣ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆)}
115113, 114eqtr3i 2760 . . . . . . . . . . . . . . . 16 ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = {𝑀 ∣ ((𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ∧ (π‘€β€˜π‘’) ∈ 𝑣) ∧ 𝑀 ∈ Xπ‘˜ ∈ 𝐴 𝑆)}
116 eqid 2730 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) = (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’))
117116mptpreima 6236 . . . . . . . . . . . . . . . . 17 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) = {𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∣ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)}
118 df-rab 3431 . . . . . . . . . . . . . . . . 17 {𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∣ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)} = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))}
119117, 118eqtri 2758 . . . . . . . . . . . . . . . 16 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) = {𝑀 ∣ (𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ∧ (π‘€β€˜π‘’) ∈ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))}
120107, 115, 1193eqtr4g 2795 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
121120eqeq2d 2741 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
122121rexbidv 3176 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
123 ineq1 4204 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑦 β†’ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))
124123imaeq2d 6058 . . . . . . . . . . . . . . 15 (𝑣 = 𝑦 β†’ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
125124eqeq2d 2741 . . . . . . . . . . . . . 14 (𝑣 = 𝑦 β†’ (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
126125cbvrexvw 3233 . . . . . . . . . . . . 13 (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑣 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
127122, 126bitrdi 286 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
128 vex 3476 . . . . . . . . . . . . . . 15 𝑦 ∈ V
129128inex1 5316 . . . . . . . . . . . . . 14 (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V
130129a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐴) ∧ 𝑦 ∈ (πΉβ€˜π‘’)) β†’ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V)
131 ovex 7444 . . . . . . . . . . . . . . . . 17 ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V
132 nfcv 2901 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘’
133 nfcv 2901 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜(πΉβ€˜π‘’)
134133, 53, 88nfov 7441 . . . . . . . . . . . . . . . . . 18 β„²π‘˜((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†)
135 fveq2 6890 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑒 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘’))
136135, 91oveq12d 7429 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ ((πΉβ€˜π‘˜) β†Ύt 𝑆) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
137132, 134, 136, 65fvmptf 7018 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ 𝐴 ∧ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ∈ V) β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
138131, 137mpan2 687 . . . . . . . . . . . . . . . 16 (𝑒 ∈ 𝐴 β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
139138adantl 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) = ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†))
140139eleq2d 2817 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↔ 𝑣 ∈ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†)))
141 nfv 1915 . . . . . . . . . . . . . . . . 17 β„²π‘˜(πœ‘ ∧ 𝑒 ∈ 𝐴)
142 nfcsb1v 3917 . . . . . . . . . . . . . . . . . 18 β„²π‘˜β¦‹π‘’ / π‘˜β¦Œπ‘Š
14388, 142nfel 2915 . . . . . . . . . . . . . . . . 17 β„²π‘˜β¦‹π‘’ / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š
144141, 143nfim 1897 . . . . . . . . . . . . . . . 16 β„²π‘˜((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š)
145 eleq1w 2814 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ (π‘˜ ∈ 𝐴 ↔ 𝑒 ∈ 𝐴))
146145anbi2d 627 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑒 β†’ ((πœ‘ ∧ π‘˜ ∈ 𝐴) ↔ (πœ‘ ∧ 𝑒 ∈ 𝐴)))
147 csbeq1a 3906 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ π‘Š = ⦋𝑒 / π‘˜β¦Œπ‘Š)
14891, 147eleq12d 2825 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑒 β†’ (𝑆 ∈ π‘Š ↔ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š))
149146, 148imbi12d 343 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑒 β†’ (((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 ∈ π‘Š) ↔ ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š)))
150144, 149, 13chvarfv 2231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š)
151 elrest 17377 . . . . . . . . . . . . . . 15 (((πΉβ€˜π‘’) ∈ V ∧ ⦋𝑒 / π‘˜β¦Œπ‘† ∈ ⦋𝑒 / π‘˜β¦Œπ‘Š) β†’ (𝑣 ∈ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
1524, 150, 151sylancr 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ ((πΉβ€˜π‘’) β†Ύt ⦋𝑒 / π‘˜β¦Œπ‘†) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
153140, 152bitrd 278 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
154 imaeq2 6054 . . . . . . . . . . . . . . 15 (𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) β†’ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)))
155154eqeq2d 2741 . . . . . . . . . . . . . 14 (𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†) β†’ (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
156155adantl 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 = (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†)) β†’ (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ↔ π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
157130, 153, 156rexxfr2d 5408 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ↔ βˆƒπ‘¦ ∈ (πΉβ€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ (𝑦 ∩ ⦋𝑒 / π‘˜β¦Œπ‘†))))
158127, 157bitr4d 281 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ 𝐴) β†’ (βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))
159158rexbidva 3174 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))
160159abbidv 2799 . . . . . . . . 9 (πœ‘ β†’ {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)} = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)})
161 eqid 2730 . . . . . . . . . . 11 (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆))
162161rnmpt 5953 . . . . . . . . . 10 ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {𝑦 ∣ βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
163 nfre1 3280 . . . . . . . . . . 11 β„²π‘₯βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)
164 nfv 1915 . . . . . . . . . . 11 β„²π‘¦βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)
16527mptex 7226 . . . . . . . . . . . . . . . 16 (𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) ∈ V
166165cnvex 7918 . . . . . . . . . . . . . . 15 β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) ∈ V
167166imaex 7909 . . . . . . . . . . . . . 14 (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∈ V
168167rgen2w 3064 . . . . . . . . . . . . 13 βˆ€π‘’ ∈ 𝐴 βˆ€π‘£ ∈ (πΉβ€˜π‘’)(β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∈ V
169 ineq1 4204 . . . . . . . . . . . . . . 15 (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) β†’ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
170169eqeq2d 2741 . . . . . . . . . . . . . 14 (π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) β†’ (𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ 𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
1716, 170rexrnmpo 7550 . . . . . . . . . . . . 13 (βˆ€π‘’ ∈ 𝐴 βˆ€π‘£ ∈ (πΉβ€˜π‘’)(β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∈ V β†’ (βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
172168, 171ax-mp 5 . . . . . . . . . . . 12 (βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆))
173 eqeq1 2734 . . . . . . . . . . . . 13 (𝑦 = π‘₯ β†’ (𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
1741732rexbidv 3217 . . . . . . . . . . . 12 (𝑦 = π‘₯ β†’ (βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)𝑦 = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
175172, 174bitrid 282 . . . . . . . . . . 11 (𝑦 = π‘₯ β†’ (βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)))
176163, 164, 175cbvabw 2804 . . . . . . . . . 10 {𝑦 ∣ βˆƒπ‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))𝑦 = (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)} = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
177162, 176eqtri 2758 . . . . . . . . 9 ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ (πΉβ€˜π‘’)π‘₯ = ((β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣) ∩ Xπ‘˜ ∈ 𝐴 𝑆)}
178 eqid 2730 . . . . . . . . . 10 (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) = (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))
179178rnmpo 7544 . . . . . . . . 9 ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) = {π‘₯ ∣ βˆƒπ‘’ ∈ 𝐴 βˆƒπ‘£ ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’)π‘₯ = (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)}
180160, 177, 1793eqtr4g 2795 . . . . . . . 8 (πœ‘ β†’ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))
18184, 180uneq12d 4163 . . . . . . 7 (πœ‘ β†’ (ran (π‘₯ ∈ {βˆͺ (∏tβ€˜πΉ)} ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) βˆͺ ran (π‘₯ ∈ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆))) = ({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))
18222, 181eqtrid 2782 . . . . . 6 (πœ‘ β†’ ran (π‘₯ ∈ ({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) ↦ (π‘₯ ∩ Xπ‘˜ ∈ 𝐴 𝑆)) = ({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))
18318, 182eqtrd 2770 . . . . 5 (πœ‘ β†’ (({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))
184183fveq2d 6894 . . . 4 (πœ‘ β†’ (fiβ€˜(({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = (fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))))
1851, 184eqtr3id 2784 . . 3 (πœ‘ β†’ ((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = (fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))))
186185fveq2d 6894 . 2 (πœ‘ β†’ (topGenβ€˜((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
187 eqid 2730 . . . . . 6 βˆͺ (∏tβ€˜πΉ) = βˆͺ (∏tβ€˜πΉ)
18872, 187, 6ptval2 23325 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟢Top) β†’ (∏tβ€˜πΉ) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
1893, 35, 188syl2anc 582 . . . 4 (πœ‘ β†’ (∏tβ€˜πΉ) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
190189oveq1d 7426 . . 3 (πœ‘ β†’ ((∏tβ€˜πΉ) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = ((topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆))
191 fvex 6903 . . . 4 (fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) ∈ V
192 tgrest 22883 . . . 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 585 . . 3 (πœ‘ β†’ (topGenβ€˜((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)) = ((topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆))
194190, 193eqtr4d 2773 . 2 (πœ‘ β†’ ((∏tβ€˜πΉ) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = (topGenβ€˜((fiβ€˜({βˆͺ (∏tβ€˜πΉ)} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ (πΉβ€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜πΉ) ↦ (π‘€β€˜π‘’)) β€œ 𝑣)))) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆)))
195 eqid 2730 . . . 4 βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))
19679, 195, 178ptval2 23325 . . 3 ((𝐴 ∈ 𝑉 ∧ (π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)):𝐴⟢Top) β†’ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
1973, 78, 196syl2anc 582 . 2 (πœ‘ β†’ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) = (topGenβ€˜(fiβ€˜({βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆)))} βˆͺ ran (𝑒 ∈ 𝐴, 𝑣 ∈ ((π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))β€˜π‘’) ↦ (β—‘(𝑀 ∈ βˆͺ (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))) ↦ (π‘€β€˜π‘’)) β€œ 𝑣))))))
198186, 194, 1973eqtr4d 2780 1 (πœ‘ β†’ ((∏tβ€˜πΉ) β†Ύt Xπ‘˜ ∈ 𝐴 𝑆) = (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ ((πΉβ€˜π‘˜) β†Ύt 𝑆))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  {cab 2707  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472  β¦‹csb 3892   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907   ↦ cmpt 5230  β—‘ccnv 5674  ran crn 5676   β€œ cima 5678   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ∈ cmpo 7413  Xcixp 8893  ficfi 9407   β†Ύt crest 17370  topGenctg 17387  βˆtcpt 17388  Topctop 22615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-ixp 8894  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9408  df-rest 17372  df-topgen 17393  df-pt 17394  df-top 22616  df-topon 22633  df-bases 22669
This theorem is referenced by:  poimirlem30  36821
  Copyright terms: Public domain W3C validator