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 35049
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 16701 . . . 4 (fi‘(({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆)) = ((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)
2 snex 5300 . . . . . . . 8 { (∏t𝐹)} ∈ V
3 ptrest.0 . . . . . . . . . 10 (𝜑𝐴𝑉)
4 fvex 6662 . . . . . . . . . . 11 (𝐹𝑢) ∈ V
54rgenw 3121 . . . . . . . . . 10 𝑢𝐴 (𝐹𝑢) ∈ V
6 eqid 2801 . . . . . . . . . . 11 (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) = (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))
76mpoexxg 7760 . . . . . . . . . 10 ((𝐴𝑉 ∧ ∀𝑢𝐴 (𝐹𝑢) ∈ V) → (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
83, 5, 7sylancl 589 . . . . . . . . 9 (𝜑 → (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
9 rnexg 7599 . . . . . . . . 9 ((𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V → ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
108, 9syl 17 . . . . . . . 8 (𝜑 → ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
11 unexg 7456 . . . . . . . 8 (({ (∏t𝐹)} ∈ V ∧ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V) → ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V)
122, 10, 11sylancr 590 . . . . . . 7 (𝜑 → ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V)
13 ptrest.2 . . . . . . . . 9 ((𝜑𝑘𝐴) → 𝑆𝑊)
1413ralrimiva 3152 . . . . . . . 8 (𝜑 → ∀𝑘𝐴 𝑆𝑊)
15 ixpexg 8473 . . . . . . . 8 (∀𝑘𝐴 𝑆𝑊X𝑘𝐴 𝑆 ∈ V)
1614, 15syl 17 . . . . . . 7 (𝜑X𝑘𝐴 𝑆 ∈ V)
17 restval 16695 . . . . . . 7 ((({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V ∧ X𝑘𝐴 𝑆 ∈ V) → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)))
1812, 16, 17syl2anc 587 . . . . . 6 (𝜑 → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)))
19 mptun 6470 . . . . . . . . 9 (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
2019rneqi 5775 . . . . . . . 8 ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ran ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
21 rnun 5975 . . . . . . . 8 ran ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))) = (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
2220, 21eqtri 2824 . . . . . . 7 ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
23 elsni 4545 . . . . . . . . . . . . . 14 (𝑥 ∈ { (∏t𝐹)} → 𝑥 = (∏t𝐹))
2423ineq1d 4141 . . . . . . . . . . . . 13 (𝑥 ∈ { (∏t𝐹)} → (𝑥X𝑘𝐴 𝑆) = ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
2524mpteq2ia 5124 . . . . . . . . . . . 12 (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = (𝑥 ∈ { (∏t𝐹)} ↦ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
26 fvex 6662 . . . . . . . . . . . . . 14 (∏t𝐹) ∈ V
2726uniex 7451 . . . . . . . . . . . . 13 (∏t𝐹) ∈ V
2827inex1 5188 . . . . . . . . . . . . 13 ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ∈ V
29 fmptsn 6910 . . . . . . . . . . . . 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 2827 . . . . . . . . . . 11 (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩}
3231rneqi 5775 . . . . . . . . . 10 ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = ran {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩}
3327rnsnop 6052 . . . . . . . . . 10 ran {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩} = {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)}
3432, 33eqtri 2824 . . . . . . . . 9 ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)}
35 ptrest.1 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐴⟶Top)
3635ffvelrnda 6832 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ Top)
37 inss1 4158 . . . . . . . . . . . . . . 15 ( (𝐹𝑘) ∩ 𝑆) ⊆ (𝐹𝑘)
38 eqid 2801 . . . . . . . . . . . . . . . 16 (𝐹𝑘) = (𝐹𝑘)
3938restuni 21770 . . . . . . . . . . . . . . 15 (((𝐹𝑘) ∈ Top ∧ ( (𝐹𝑘) ∩ 𝑆) ⊆ (𝐹𝑘)) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4036, 37, 39sylancl 589 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
41 fvex 6662 . . . . . . . . . . . . . . . . 17 (𝐹𝑘) ∈ V
4238restin 21774 . . . . . . . . . . . . . . . . 17 (((𝐹𝑘) ∈ V ∧ 𝑆𝑊) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))))
4341, 13, 42sylancr 590 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))))
44 incom 4131 . . . . . . . . . . . . . . . . 17 (𝑆 (𝐹𝑘)) = ( (𝐹𝑘) ∩ 𝑆)
4544oveq2i 7150 . . . . . . . . . . . . . . . 16 ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆))
4643, 45eqtrdi 2852 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4746unieqd 4817 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4840, 47eqtr4d 2839 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t 𝑆))
4948ixpeq2dva 8463 . . . . . . . . . . . 12 (𝜑X𝑘𝐴 ( (𝐹𝑘) ∩ 𝑆) = X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆))
50 ixpin 8474 . . . . . . . . . . . 12 X𝑘𝐴 ( (𝐹𝑘) ∩ 𝑆) = (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆)
51 nfcv 2958 . . . . . . . . . . . . . 14 𝑦 ((𝐹𝑘) ↾t 𝑆)
52 nfcv 2958 . . . . . . . . . . . . . . . 16 𝑘(𝐹𝑦)
53 nfcv 2958 . . . . . . . . . . . . . . . 16 𝑘t
54 nfcsb1v 3855 . . . . . . . . . . . . . . . 16 𝑘𝑦 / 𝑘𝑆
5552, 53, 54nfov 7169 . . . . . . . . . . . . . . 15 𝑘((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
5655nfuni 4810 . . . . . . . . . . . . . 14 𝑘 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
57 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (𝐹𝑘) = (𝐹𝑦))
58 csbeq1a 3845 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦𝑆 = 𝑦 / 𝑘𝑆)
5957, 58oveq12d 7157 . . . . . . . . . . . . . . 15 (𝑘 = 𝑦 → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6059unieqd 4817 . . . . . . . . . . . . . 14 (𝑘 = 𝑦 ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6151, 56, 60cbvixp 8465 . . . . . . . . . . . . 13 X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
62 ixpeq2 8462 . . . . . . . . . . . . . 14 (∀𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) → X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
63 ovex 7172 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) ∈ V
64 nfcv 2958 . . . . . . . . . . . . . . . . 17 𝑘𝑦
65 eqid 2801 . . . . . . . . . . . . . . . . 17 (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)) = (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))
6664, 55, 59, 65fvmptf 6770 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) ∈ V) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6763, 66mpan2 690 . . . . . . . . . . . . . . 15 (𝑦𝐴 → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6867unieqd 4817 . . . . . . . . . . . . . 14 (𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6962, 68mprg 3123 . . . . . . . . . . . . 13 X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
7061, 69eqtr4i 2827 . . . . . . . . . . . 12 X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆) = X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦)
7149, 50, 703eqtr3g 2859 . . . . . . . . . . 11 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆) = X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦))
72 eqid 2801 . . . . . . . . . . . . . 14 (∏t𝐹) = (∏t𝐹)
7372ptuni 22202 . . . . . . . . . . . . 13 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
743, 35, 73syl2anc 587 . . . . . . . . . . . 12 (𝜑X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
7574ineq1d 4141 . . . . . . . . . . 11 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆) = ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
76 resttop 21768 . . . . . . . . . . . . . 14 (((𝐹𝑘) ∈ Top ∧ 𝑆𝑊) → ((𝐹𝑘) ↾t 𝑆) ∈ Top)
7736, 13, 76syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) ∈ Top)
7877fmpttd 6860 . . . . . . . . . . . 12 (𝜑 → (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top)
79 eqid 2801 . . . . . . . . . . . . 13 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))
8079ptuni 22202 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
813, 78, 80syl2anc 587 . . . . . . . . . . 11 (𝜑X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
8271, 75, 813eqtr3d 2844 . . . . . . . . . 10 (𝜑 → ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
8382sneqd 4540 . . . . . . . . 9 (𝜑 → {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)} = { (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))})
8434, 83syl5eq 2848 . . . . . . . 8 (𝜑 → ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = { (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))})
85 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
8685elixp 8455 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤X𝑘𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆))
8786simprbi 500 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤X𝑘𝐴 𝑆 → ∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆)
88 nfcsb1v 3855 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝑢 / 𝑘𝑆
8988nfel2 2976 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝑤𝑢) ∈ 𝑢 / 𝑘𝑆
90 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑢 → (𝑤𝑘) = (𝑤𝑢))
91 csbeq1a 3845 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑢𝑆 = 𝑢 / 𝑘𝑆)
9290, 91eleq12d 2887 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑢 → ((𝑤𝑘) ∈ 𝑆 ↔ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9389, 92rspc 3562 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢𝐴 → (∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆 → (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9487, 93syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑢𝐴 → (𝑤X𝑘𝐴 𝑆 → (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9594pm4.71d 565 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝐴 → (𝑤X𝑘𝐴 𝑆 ↔ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
9695anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑢𝐴 → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))))
97 an4 655 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
98 elin 3900 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆) ↔ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9998anbi2i 625 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
10097, 99bitr4i 281 . . . . . . . . . . . . . . . . . . 19 (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)))
10196, 100syl6bb 290 . . . . . . . . . . . . . . . . . 18 (𝑢𝐴 → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
102 elin 3900 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ↔ (𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆))
10382eleq2d 2878 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑤 ∈ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ↔ 𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))))
104102, 103bitr3id 288 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ↔ 𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))))
105104anbi1d 632 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)) ↔ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
106101, 105sylan9bbr 514 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝐴) → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
107106abbidv 2865 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝐴) → {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)} = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))})
108 eqid 2801 . . . . . . . . . . . . . . . . . . . 20 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) = (𝑤 (∏t𝐹) ↦ (𝑤𝑢))
109108mptpreima 6063 . . . . . . . . . . . . . . . . . . 19 ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) = {𝑤 (∏t𝐹) ∣ (𝑤𝑢) ∈ 𝑣}
110 df-rab 3118 . . . . . . . . . . . . . . . . . . 19 {𝑤 (∏t𝐹) ∣ (𝑤𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)}
111109, 110eqtr2i 2825 . . . . . . . . . . . . . . . . . 18 {𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)
112 abid2 2935 . . . . . . . . . . . . . . . . . 18 {𝑤𝑤X𝑘𝐴 𝑆} = X𝑘𝐴 𝑆
113111, 112ineq12i 4140 . . . . . . . . . . . . . . . . 17 ({𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} ∩ {𝑤𝑤X𝑘𝐴 𝑆}) = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)
114 inab 4226 . . . . . . . . . . . . . . . . 17 ({𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} ∩ {𝑤𝑤X𝑘𝐴 𝑆}) = {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)}
115113, 114eqtr3i 2826 . . . . . . . . . . . . . . . 16 (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) = {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)}
116 eqid 2801 . . . . . . . . . . . . . . . . . 18 (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) = (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢))
117116mptpreima 6063 . . . . . . . . . . . . . . . . 17 ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = {𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∣ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)}
118 df-rab 3118 . . . . . . . . . . . . . . . . 17 {𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∣ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)} = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))}
119117, 118eqtri 2824 . . . . . . . . . . . . . . . 16 ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))}
120107, 115, 1193eqtr4g 2861 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)))
121120eqeq2d 2812 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆))))
122121rexbidv 3259 . . . . . . . . . . . . 13 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆))))
123 ineq1 4134 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑦 → (𝑣𝑢 / 𝑘𝑆) = (𝑦𝑢 / 𝑘𝑆))
124123imaeq2d 5900 . . . . . . . . . . . . . . 15 (𝑣 = 𝑦 → ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
125124eqeq2d 2812 . . . . . . . . . . . . . 14 (𝑣 = 𝑦 → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
126125cbvrexvw 3400 . . . . . . . . . . . . 13 (∃𝑣 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
127122, 126syl6bb 290 . . . . . . . . . . . 12 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
128 vex 3447 . . . . . . . . . . . . . . 15 𝑦 ∈ V
129128inex1 5188 . . . . . . . . . . . . . 14 (𝑦𝑢 / 𝑘𝑆) ∈ V
130129a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑢𝐴) ∧ 𝑦 ∈ (𝐹𝑢)) → (𝑦𝑢 / 𝑘𝑆) ∈ V)
131 ovex 7172 . . . . . . . . . . . . . . . . 17 ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ∈ V
132 nfcv 2958 . . . . . . . . . . . . . . . . . 18 𝑘𝑢
133 nfcv 2958 . . . . . . . . . . . . . . . . . . 19 𝑘(𝐹𝑢)
134133, 53, 88nfov 7169 . . . . . . . . . . . . . . . . . 18 𝑘((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆)
135 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝐹𝑘) = (𝐹𝑢))
136135, 91oveq12d 7157 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
137132, 134, 136, 65fvmptf 6770 . . . . . . . . . . . . . . . . 17 ((𝑢𝐴 ∧ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ∈ V) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
138131, 137mpan2 690 . . . . . . . . . . . . . . . 16 (𝑢𝐴 → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
139138adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
140139eleq2d 2878 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆)))
141 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑘(𝜑𝑢𝐴)
142 nfcsb1v 3855 . . . . . . . . . . . . . . . . . 18 𝑘𝑢 / 𝑘𝑊
14388, 142nfel 2972 . . . . . . . . . . . . . . . . 17 𝑘𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊
144141, 143nfim 1897 . . . . . . . . . . . . . . . 16 𝑘((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)
145 eleq1w 2875 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 → (𝑘𝐴𝑢𝐴))
146145anbi2d 631 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ((𝜑𝑘𝐴) ↔ (𝜑𝑢𝐴)))
147 csbeq1a 3845 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢𝑊 = 𝑢 / 𝑘𝑊)
14891, 147eleq12d 2887 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → (𝑆𝑊𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊))
149146, 148imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (((𝜑𝑘𝐴) → 𝑆𝑊) ↔ ((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)))
150144, 149, 13chvarfv 2241 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)
151 elrest 16696 . . . . . . . . . . . . . . 15 (((𝐹𝑢) ∈ V ∧ 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊) → (𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
1524, 150, 151sylancr 590 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
153140, 152bitrd 282 . . . . . . . . . . . . 13 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
154 imaeq2 5896 . . . . . . . . . . . . . . 15 (𝑣 = (𝑦𝑢 / 𝑘𝑆) → ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
155154eqeq2d 2812 . . . . . . . . . . . . . 14 (𝑣 = (𝑦𝑢 / 𝑘𝑆) → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
156155adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑢𝐴) ∧ 𝑣 = (𝑦𝑢 / 𝑘𝑆)) → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
157130, 153, 156rexxfr2d 5280 . . . . . . . . . . . 12 ((𝜑𝑢𝐴) → (∃𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
158127, 157bitr4d 285 . . . . . . . . . . 11 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
159158rexbidva 3258 . . . . . . . . . 10 (𝜑 → (∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
160159abbidv 2865 . . . . . . . . 9 (𝜑 → {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)} = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)})
161 eqid 2801 . . . . . . . . . . 11 (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))
162161rnmpt 5795 . . . . . . . . . 10 ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)}
163 nfre1 3268 . . . . . . . . . . 11 𝑥𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)
164 nfv 1915 . . . . . . . . . . 11 𝑦𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)
16527mptex 6967 . . . . . . . . . . . . . . . 16 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) ∈ V
166165cnvex 7616 . . . . . . . . . . . . . . 15 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) ∈ V
167166imaex 7607 . . . . . . . . . . . . . 14 ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V
168167rgen2w 3122 . . . . . . . . . . . . 13 𝑢𝐴𝑣 ∈ (𝐹𝑢)((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V
169 ineq1 4134 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) → (𝑥X𝑘𝐴 𝑆) = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆))
170169eqeq2d 2812 . . . . . . . . . . . . . 14 (𝑥 = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) → (𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ 𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
1716, 170rexrnmpo 7273 . . . . . . . . . . . . 13 (∀𝑢𝐴𝑣 ∈ (𝐹𝑢)((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V → (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
172168, 171ax-mp 5 . . . . . . . . . . . 12 (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆))
173 eqeq1 2805 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ 𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
1741732rexbidv 3262 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
175172, 174syl5bb 286 . . . . . . . . . . 11 (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
176163, 164, 175cbvabw 2870 . . . . . . . . . 10 {𝑦 ∣ ∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)} = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)}
177162, 176eqtri 2824 . . . . . . . . 9 ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)}
178 eqid 2801 . . . . . . . . . 10 (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)) = (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))
179178rnmpo 7267 . . . . . . . . 9 ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)}
180160, 177, 1793eqtr4g 2861 . . . . . . . 8 (𝜑 → ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
18184, 180uneq12d 4094 . . . . . . 7 (𝜑 → (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
18222, 181syl5eq 2848 . . . . . 6 (𝜑 → ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
18318, 182eqtrd 2836 . . . . 5 (𝜑 → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
184183fveq2d 6653 . . . 4 (𝜑 → (fi‘(({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆)) = (fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))))
1851, 184syl5eqr 2850 . . 3 (𝜑 → ((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆) = (fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))))
186185fveq2d 6653 . 2 (𝜑 → (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
187 eqid 2801 . . . . . 6 (∏t𝐹) = (∏t𝐹)
18872, 187, 6ptval2 22209 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) = (topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))))
1893, 35, 188syl2anc 587 . . . 4 (𝜑 → (∏t𝐹) = (topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))))
190189oveq1d 7154 . . 3 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = ((topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))) ↾t X𝑘𝐴 𝑆))
191 fvex 6662 . . . 4 (fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ∈ V
192 tgrest 21767 . . . 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 590 . . 3 (𝜑 → (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)) = ((topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))) ↾t X𝑘𝐴 𝑆))
194190, 193eqtr4d 2839 . 2 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)))
195 eqid 2801 . . . 4 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))
19679, 195, 178ptval2 22209 . . 3 ((𝐴𝑉 ∧ (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top) → (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
1973, 78, 196syl2anc 587 . 2 (𝜑 → (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
198186, 194, 1973eqtr4d 2846 1 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  {cab 2779  wral 3109  wrex 3110  {crab 3113  Vcvv 3444  csb 3831  cun 3882  cin 3883  wss 3884  {csn 4528  cop 4534   cuni 4803  cmpt 5113  ccnv 5522  ran crn 5524  cima 5526   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7139  cmpo 7141  Xcixp 8448  ficfi 8862  t crest 16689  topGenctg 16706  tcpt 16707  Topctop 21501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-ixp 8449  df-en 8497  df-dom 8498  df-fin 8500  df-fi 8863  df-rest 16691  df-topgen 16712  df-pt 16713  df-top 21502  df-topon 21519  df-bases 21554
This theorem is referenced by:  poimirlem30  35080
  Copyright terms: Public domain W3C validator