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 37626
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 17477 . . . 4 (fi‘(({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆)) = ((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)
2 snex 5436 . . . . . . . 8 { (∏t𝐹)} ∈ V
3 ptrest.0 . . . . . . . . . 10 (𝜑𝐴𝑉)
4 fvex 6919 . . . . . . . . . . 11 (𝐹𝑢) ∈ V
54rgenw 3065 . . . . . . . . . 10 𝑢𝐴 (𝐹𝑢) ∈ V
6 eqid 2737 . . . . . . . . . . 11 (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) = (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))
76mpoexxg 8100 . . . . . . . . . 10 ((𝐴𝑉 ∧ ∀𝑢𝐴 (𝐹𝑢) ∈ V) → (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
83, 5, 7sylancl 586 . . . . . . . . 9 (𝜑 → (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
9 rnexg 7924 . . . . . . . . 9 ((𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V → ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
108, 9syl 17 . . . . . . . 8 (𝜑 → ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
11 unexg 7763 . . . . . . . 8 (({ (∏t𝐹)} ∈ V ∧ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V) → ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V)
122, 10, 11sylancr 587 . . . . . . 7 (𝜑 → ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V)
13 ptrest.2 . . . . . . . . 9 ((𝜑𝑘𝐴) → 𝑆𝑊)
1413ralrimiva 3146 . . . . . . . 8 (𝜑 → ∀𝑘𝐴 𝑆𝑊)
15 ixpexg 8962 . . . . . . . 8 (∀𝑘𝐴 𝑆𝑊X𝑘𝐴 𝑆 ∈ V)
1614, 15syl 17 . . . . . . 7 (𝜑X𝑘𝐴 𝑆 ∈ V)
17 restval 17471 . . . . . . 7 ((({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V ∧ X𝑘𝐴 𝑆 ∈ V) → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)))
1812, 16, 17syl2anc 584 . . . . . 6 (𝜑 → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)))
19 mptun 6714 . . . . . . . . 9 (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
2019rneqi 5948 . . . . . . . 8 ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ran ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
21 rnun 6165 . . . . . . . 8 ran ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))) = (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
2220, 21eqtri 2765 . . . . . . 7 ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
23 elsni 4643 . . . . . . . . . . . . . 14 (𝑥 ∈ { (∏t𝐹)} → 𝑥 = (∏t𝐹))
2423ineq1d 4219 . . . . . . . . . . . . 13 (𝑥 ∈ { (∏t𝐹)} → (𝑥X𝑘𝐴 𝑆) = ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
2524mpteq2ia 5245 . . . . . . . . . . . 12 (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = (𝑥 ∈ { (∏t𝐹)} ↦ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
26 fvex 6919 . . . . . . . . . . . . . 14 (∏t𝐹) ∈ V
2726uniex 7761 . . . . . . . . . . . . 13 (∏t𝐹) ∈ V
2827inex1 5317 . . . . . . . . . . . . 13 ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ∈ V
29 fmptsn 7187 . . . . . . . . . . . . 13 (( (∏t𝐹) ∈ V ∧ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ∈ V) → {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩} = (𝑥 ∈ { (∏t𝐹)} ↦ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)))
3027, 28, 29mp2an 692 . . . . . . . . . . . 12 {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩} = (𝑥 ∈ { (∏t𝐹)} ↦ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
3125, 30eqtr4i 2768 . . . . . . . . . . 11 (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩}
3231rneqi 5948 . . . . . . . . . 10 ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = ran {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩}
3327rnsnop 6244 . . . . . . . . . 10 ran {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩} = {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)}
3432, 33eqtri 2765 . . . . . . . . 9 ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)}
35 ptrest.1 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐴⟶Top)
3635ffvelcdmda 7104 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ Top)
37 inss1 4237 . . . . . . . . . . . . . . 15 ( (𝐹𝑘) ∩ 𝑆) ⊆ (𝐹𝑘)
38 eqid 2737 . . . . . . . . . . . . . . . 16 (𝐹𝑘) = (𝐹𝑘)
3938restuni 23170 . . . . . . . . . . . . . . 15 (((𝐹𝑘) ∈ Top ∧ ( (𝐹𝑘) ∩ 𝑆) ⊆ (𝐹𝑘)) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4036, 37, 39sylancl 586 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
41 fvex 6919 . . . . . . . . . . . . . . . . 17 (𝐹𝑘) ∈ V
4238restin 23174 . . . . . . . . . . . . . . . . 17 (((𝐹𝑘) ∈ V ∧ 𝑆𝑊) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))))
4341, 13, 42sylancr 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))))
44 incom 4209 . . . . . . . . . . . . . . . . 17 (𝑆 (𝐹𝑘)) = ( (𝐹𝑘) ∩ 𝑆)
4544oveq2i 7442 . . . . . . . . . . . . . . . 16 ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆))
4643, 45eqtrdi 2793 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4746unieqd 4920 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4840, 47eqtr4d 2780 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t 𝑆))
4948ixpeq2dva 8952 . . . . . . . . . . . 12 (𝜑X𝑘𝐴 ( (𝐹𝑘) ∩ 𝑆) = X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆))
50 ixpin 8963 . . . . . . . . . . . 12 X𝑘𝐴 ( (𝐹𝑘) ∩ 𝑆) = (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆)
51 nfcv 2905 . . . . . . . . . . . . . 14 𝑦 ((𝐹𝑘) ↾t 𝑆)
52 nfcv 2905 . . . . . . . . . . . . . . . 16 𝑘(𝐹𝑦)
53 nfcv 2905 . . . . . . . . . . . . . . . 16 𝑘t
54 nfcsb1v 3923 . . . . . . . . . . . . . . . 16 𝑘𝑦 / 𝑘𝑆
5552, 53, 54nfov 7461 . . . . . . . . . . . . . . 15 𝑘((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
5655nfuni 4914 . . . . . . . . . . . . . 14 𝑘 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
57 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (𝐹𝑘) = (𝐹𝑦))
58 csbeq1a 3913 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦𝑆 = 𝑦 / 𝑘𝑆)
5957, 58oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑘 = 𝑦 → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6059unieqd 4920 . . . . . . . . . . . . . 14 (𝑘 = 𝑦 ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6151, 56, 60cbvixp 8954 . . . . . . . . . . . . 13 X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
62 ixpeq2 8951 . . . . . . . . . . . . . 14 (∀𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) → X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
63 ovex 7464 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) ∈ V
64 nfcv 2905 . . . . . . . . . . . . . . . . 17 𝑘𝑦
65 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)) = (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))
6664, 55, 59, 65fvmptf 7037 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) ∈ V) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6763, 66mpan2 691 . . . . . . . . . . . . . . 15 (𝑦𝐴 → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6867unieqd 4920 . . . . . . . . . . . . . 14 (𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6962, 68mprg 3067 . . . . . . . . . . . . 13 X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
7061, 69eqtr4i 2768 . . . . . . . . . . . 12 X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆) = X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦)
7149, 50, 703eqtr3g 2800 . . . . . . . . . . 11 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆) = X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦))
72 eqid 2737 . . . . . . . . . . . . . 14 (∏t𝐹) = (∏t𝐹)
7372ptuni 23602 . . . . . . . . . . . . 13 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
743, 35, 73syl2anc 584 . . . . . . . . . . . 12 (𝜑X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
7574ineq1d 4219 . . . . . . . . . . 11 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆) = ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
76 resttop 23168 . . . . . . . . . . . . . 14 (((𝐹𝑘) ∈ Top ∧ 𝑆𝑊) → ((𝐹𝑘) ↾t 𝑆) ∈ Top)
7736, 13, 76syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) ∈ Top)
7877fmpttd 7135 . . . . . . . . . . . 12 (𝜑 → (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top)
79 eqid 2737 . . . . . . . . . . . . 13 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))
8079ptuni 23602 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
813, 78, 80syl2anc 584 . . . . . . . . . . 11 (𝜑X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
8271, 75, 813eqtr3d 2785 . . . . . . . . . 10 (𝜑 → ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
8382sneqd 4638 . . . . . . . . 9 (𝜑 → {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)} = { (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))})
8434, 83eqtrid 2789 . . . . . . . 8 (𝜑 → ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = { (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))})
85 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
8685elixp 8944 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤X𝑘𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆))
8786simprbi 496 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤X𝑘𝐴 𝑆 → ∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆)
88 nfcsb1v 3923 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝑢 / 𝑘𝑆
8988nfel2 2924 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝑤𝑢) ∈ 𝑢 / 𝑘𝑆
90 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑢 → (𝑤𝑘) = (𝑤𝑢))
91 csbeq1a 3913 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑢𝑆 = 𝑢 / 𝑘𝑆)
9290, 91eleq12d 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑢 → ((𝑤𝑘) ∈ 𝑆 ↔ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9389, 92rspc 3610 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢𝐴 → (∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆 → (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9487, 93syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑢𝐴 → (𝑤X𝑘𝐴 𝑆 → (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9594pm4.71d 561 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝐴 → (𝑤X𝑘𝐴 𝑆 ↔ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
9695anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (𝑢𝐴 → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))))
97 an4 656 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
98 elin 3967 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆) ↔ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9998anbi2i 623 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
10097, 99bitr4i 278 . . . . . . . . . . . . . . . . . . 19 (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)))
10196, 100bitrdi 287 . . . . . . . . . . . . . . . . . 18 (𝑢𝐴 → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
102 elin 3967 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ↔ (𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆))
10382eleq2d 2827 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑤 ∈ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ↔ 𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))))
104102, 103bitr3id 285 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ↔ 𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))))
105104anbi1d 631 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)) ↔ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
106101, 105sylan9bbr 510 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝐴) → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
107106abbidv 2808 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝐴) → {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)} = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))})
108 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) = (𝑤 (∏t𝐹) ↦ (𝑤𝑢))
109108mptpreima 6258 . . . . . . . . . . . . . . . . . . 19 ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) = {𝑤 (∏t𝐹) ∣ (𝑤𝑢) ∈ 𝑣}
110 df-rab 3437 . . . . . . . . . . . . . . . . . . 19 {𝑤 (∏t𝐹) ∣ (𝑤𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)}
111109, 110eqtr2i 2766 . . . . . . . . . . . . . . . . . 18 {𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)
112 abid2 2879 . . . . . . . . . . . . . . . . . 18 {𝑤𝑤X𝑘𝐴 𝑆} = X𝑘𝐴 𝑆
113111, 112ineq12i 4218 . . . . . . . . . . . . . . . . 17 ({𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} ∩ {𝑤𝑤X𝑘𝐴 𝑆}) = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)
114 inab 4309 . . . . . . . . . . . . . . . . 17 ({𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} ∩ {𝑤𝑤X𝑘𝐴 𝑆}) = {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)}
115113, 114eqtr3i 2767 . . . . . . . . . . . . . . . 16 (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) = {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)}
116 eqid 2737 . . . . . . . . . . . . . . . . . 18 (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) = (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢))
117116mptpreima 6258 . . . . . . . . . . . . . . . . 17 ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = {𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∣ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)}
118 df-rab 3437 . . . . . . . . . . . . . . . . 17 {𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∣ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)} = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))}
119117, 118eqtri 2765 . . . . . . . . . . . . . . . 16 ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))}
120107, 115, 1193eqtr4g 2802 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)))
121120eqeq2d 2748 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆))))
122121rexbidv 3179 . . . . . . . . . . . . 13 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆))))
123 ineq1 4213 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑦 → (𝑣𝑢 / 𝑘𝑆) = (𝑦𝑢 / 𝑘𝑆))
124123imaeq2d 6078 . . . . . . . . . . . . . . 15 (𝑣 = 𝑦 → ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
125124eqeq2d 2748 . . . . . . . . . . . . . 14 (𝑣 = 𝑦 → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
126125cbvrexvw 3238 . . . . . . . . . . . . 13 (∃𝑣 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
127122, 126bitrdi 287 . . . . . . . . . . . 12 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
128 vex 3484 . . . . . . . . . . . . . . 15 𝑦 ∈ V
129128inex1 5317 . . . . . . . . . . . . . 14 (𝑦𝑢 / 𝑘𝑆) ∈ V
130129a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑢𝐴) ∧ 𝑦 ∈ (𝐹𝑢)) → (𝑦𝑢 / 𝑘𝑆) ∈ V)
131 ovex 7464 . . . . . . . . . . . . . . . . 17 ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ∈ V
132 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑘𝑢
133 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑘(𝐹𝑢)
134133, 53, 88nfov 7461 . . . . . . . . . . . . . . . . . 18 𝑘((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆)
135 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝐹𝑘) = (𝐹𝑢))
136135, 91oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
137132, 134, 136, 65fvmptf 7037 . . . . . . . . . . . . . . . . 17 ((𝑢𝐴 ∧ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ∈ V) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
138131, 137mpan2 691 . . . . . . . . . . . . . . . 16 (𝑢𝐴 → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
139138adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
140139eleq2d 2827 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆)))
141 nfv 1914 . . . . . . . . . . . . . . . . 17 𝑘(𝜑𝑢𝐴)
142 nfcsb1v 3923 . . . . . . . . . . . . . . . . . 18 𝑘𝑢 / 𝑘𝑊
14388, 142nfel 2920 . . . . . . . . . . . . . . . . 17 𝑘𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊
144141, 143nfim 1896 . . . . . . . . . . . . . . . 16 𝑘((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)
145 eleq1w 2824 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 → (𝑘𝐴𝑢𝐴))
146145anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ((𝜑𝑘𝐴) ↔ (𝜑𝑢𝐴)))
147 csbeq1a 3913 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢𝑊 = 𝑢 / 𝑘𝑊)
14891, 147eleq12d 2835 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → (𝑆𝑊𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊))
149146, 148imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (((𝜑𝑘𝐴) → 𝑆𝑊) ↔ ((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)))
150144, 149, 13chvarfv 2240 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)
151 elrest 17472 . . . . . . . . . . . . . . 15 (((𝐹𝑢) ∈ V ∧ 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊) → (𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
1524, 150, 151sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
153140, 152bitrd 279 . . . . . . . . . . . . 13 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
154 imaeq2 6074 . . . . . . . . . . . . . . 15 (𝑣 = (𝑦𝑢 / 𝑘𝑆) → ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
155154eqeq2d 2748 . . . . . . . . . . . . . 14 (𝑣 = (𝑦𝑢 / 𝑘𝑆) → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
156155adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑢𝐴) ∧ 𝑣 = (𝑦𝑢 / 𝑘𝑆)) → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
157130, 153, 156rexxfr2d 5411 . . . . . . . . . . . 12 ((𝜑𝑢𝐴) → (∃𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
158127, 157bitr4d 282 . . . . . . . . . . 11 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
159158rexbidva 3177 . . . . . . . . . 10 (𝜑 → (∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
160159abbidv 2808 . . . . . . . . 9 (𝜑 → {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)} = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)})
161 eqid 2737 . . . . . . . . . . 11 (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))
162161rnmpt 5968 . . . . . . . . . 10 ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)}
163 nfre1 3285 . . . . . . . . . . 11 𝑥𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)
164 nfv 1914 . . . . . . . . . . 11 𝑦𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)
16527mptex 7243 . . . . . . . . . . . . . . . 16 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) ∈ V
166165cnvex 7947 . . . . . . . . . . . . . . 15 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) ∈ V
167166imaex 7936 . . . . . . . . . . . . . 14 ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V
168167rgen2w 3066 . . . . . . . . . . . . 13 𝑢𝐴𝑣 ∈ (𝐹𝑢)((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V
169 ineq1 4213 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) → (𝑥X𝑘𝐴 𝑆) = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆))
170169eqeq2d 2748 . . . . . . . . . . . . . 14 (𝑥 = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) → (𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ 𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
1716, 170rexrnmpo 7573 . . . . . . . . . . . . 13 (∀𝑢𝐴𝑣 ∈ (𝐹𝑢)((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V → (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
172168, 171ax-mp 5 . . . . . . . . . . . 12 (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆))
173 eqeq1 2741 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ 𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
1741732rexbidv 3222 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
175172, 174bitrid 283 . . . . . . . . . . 11 (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
176163, 164, 175cbvabw 2813 . . . . . . . . . 10 {𝑦 ∣ ∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)} = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)}
177162, 176eqtri 2765 . . . . . . . . 9 ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)}
178 eqid 2737 . . . . . . . . . 10 (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)) = (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))
179178rnmpo 7566 . . . . . . . . 9 ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)}
180160, 177, 1793eqtr4g 2802 . . . . . . . 8 (𝜑 → ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
18184, 180uneq12d 4169 . . . . . . 7 (𝜑 → (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
18222, 181eqtrid 2789 . . . . . 6 (𝜑 → ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
18318, 182eqtrd 2777 . . . . 5 (𝜑 → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
184183fveq2d 6910 . . . 4 (𝜑 → (fi‘(({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆)) = (fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))))
1851, 184eqtr3id 2791 . . 3 (𝜑 → ((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆) = (fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))))
186185fveq2d 6910 . 2 (𝜑 → (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
187 eqid 2737 . . . . . 6 (∏t𝐹) = (∏t𝐹)
18872, 187, 6ptval2 23609 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) = (topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))))
1893, 35, 188syl2anc 584 . . . 4 (𝜑 → (∏t𝐹) = (topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))))
190189oveq1d 7446 . . 3 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = ((topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))) ↾t X𝑘𝐴 𝑆))
191 fvex 6919 . . . 4 (fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ∈ V
192 tgrest 23167 . . . 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 587 . . 3 (𝜑 → (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)) = ((topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))) ↾t X𝑘𝐴 𝑆))
194190, 193eqtr4d 2780 . 2 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)))
195 eqid 2737 . . . 4 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))
19679, 195, 178ptval2 23609 . . 3 ((𝐴𝑉 ∧ (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top) → (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
1973, 78, 196syl2anc 584 . 2 (𝜑 → (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
198186, 194, 1973eqtr4d 2787 1 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  csb 3899  cun 3949  cin 3950  wss 3951  {csn 4626  cop 4632   cuni 4907  cmpt 5225  ccnv 5684  ran crn 5686  cima 5688   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  Xcixp 8937  ficfi 9450  t crest 17465  topGenctg 17482  tcpt 17483  Topctop 22899
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-1o 8506  df-2o 8507  df-ixp 8938  df-en 8986  df-dom 8987  df-fin 8989  df-fi 9451  df-rest 17467  df-topgen 17488  df-pt 17489  df-top 22900  df-topon 22917  df-bases 22953
This theorem is referenced by:  poimirlem30  37657
  Copyright terms: Public domain W3C validator