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 32361
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 15864 . . . 4 (fi‘(({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆)) = ((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)
2 snex 4829 . . . . . . . 8 { (∏t𝐹)} ∈ V
3 ptrest.0 . . . . . . . . . 10 (𝜑𝐴𝑉)
4 fvex 6097 . . . . . . . . . . 11 (𝐹𝑢) ∈ V
54rgenw 2907 . . . . . . . . . 10 𝑢𝐴 (𝐹𝑢) ∈ V
6 eqid 2609 . . . . . . . . . . 11 (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) = (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))
76mpt2exxg 7110 . . . . . . . . . 10 ((𝐴𝑉 ∧ ∀𝑢𝐴 (𝐹𝑢) ∈ V) → (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
83, 5, 7sylancl 692 . . . . . . . . 9 (𝜑 → (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
9 rnexg 6967 . . . . . . . . 9 ((𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V → ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
108, 9syl 17 . . . . . . . 8 (𝜑 → ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V)
11 unexg 6834 . . . . . . . 8 (({ (∏t𝐹)} ∈ V ∧ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ∈ V) → ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V)
122, 10, 11sylancr 693 . . . . . . 7 (𝜑 → ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V)
13 ptrest.2 . . . . . . . . 9 ((𝜑𝑘𝐴) → 𝑆𝑊)
1413ralrimiva 2948 . . . . . . . 8 (𝜑 → ∀𝑘𝐴 𝑆𝑊)
15 ixpexg 7795 . . . . . . . 8 (∀𝑘𝐴 𝑆𝑊X𝑘𝐴 𝑆 ∈ V)
1614, 15syl 17 . . . . . . 7 (𝜑X𝑘𝐴 𝑆 ∈ V)
17 restval 15858 . . . . . . 7 ((({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ∈ V ∧ X𝑘𝐴 𝑆 ∈ V) → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)))
1812, 16, 17syl2anc 690 . . . . . 6 (𝜑 → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)))
19 mptun 5923 . . . . . . . . 9 (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
2019rneqi 5259 . . . . . . . 8 ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ran ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
21 rnun 5445 . . . . . . . 8 ran ((𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))) = (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
2220, 21eqtri 2631 . . . . . . 7 ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)))
23 elsni 4141 . . . . . . . . . . . . . 14 (𝑥 ∈ { (∏t𝐹)} → 𝑥 = (∏t𝐹))
2423ineq1d 3774 . . . . . . . . . . . . 13 (𝑥 ∈ { (∏t𝐹)} → (𝑥X𝑘𝐴 𝑆) = ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
2524mpteq2ia 4662 . . . . . . . . . . . 12 (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = (𝑥 ∈ { (∏t𝐹)} ↦ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
26 fvex 6097 . . . . . . . . . . . . . 14 (∏t𝐹) ∈ V
2726uniex 6828 . . . . . . . . . . . . 13 (∏t𝐹) ∈ V
2827inex1 4721 . . . . . . . . . . . . 13 ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ∈ V
29 fmptsn 6315 . . . . . . . . . . . . 13 (( (∏t𝐹) ∈ V ∧ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ∈ V) → {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩} = (𝑥 ∈ { (∏t𝐹)} ↦ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)))
3027, 28, 29mp2an 703 . . . . . . . . . . . 12 {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩} = (𝑥 ∈ { (∏t𝐹)} ↦ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
3125, 30eqtr4i 2634 . . . . . . . . . . 11 (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩}
3231rneqi 5259 . . . . . . . . . 10 ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = ran {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩}
3327rnsnop 5519 . . . . . . . . . 10 ran {⟨ (∏t𝐹), ( (∏t𝐹) ∩ X𝑘𝐴 𝑆)⟩} = {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)}
3432, 33eqtri 2631 . . . . . . . . 9 ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)}
35 ptrest.1 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐴⟶Top)
3635ffvelrnda 6251 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ Top)
37 inss1 3794 . . . . . . . . . . . . . . 15 ( (𝐹𝑘) ∩ 𝑆) ⊆ (𝐹𝑘)
38 eqid 2609 . . . . . . . . . . . . . . . 16 (𝐹𝑘) = (𝐹𝑘)
3938restuni 20723 . . . . . . . . . . . . . . 15 (((𝐹𝑘) ∈ Top ∧ ( (𝐹𝑘) ∩ 𝑆) ⊆ (𝐹𝑘)) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4036, 37, 39sylancl 692 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
41 fvex 6097 . . . . . . . . . . . . . . . . 17 (𝐹𝑘) ∈ V
4238restin 20727 . . . . . . . . . . . . . . . . 17 (((𝐹𝑘) ∈ V ∧ 𝑆𝑊) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))))
4341, 13, 42sylancr 693 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))))
44 incom 3766 . . . . . . . . . . . . . . . . 17 (𝑆 (𝐹𝑘)) = ( (𝐹𝑘) ∩ 𝑆)
4544oveq2i 6537 . . . . . . . . . . . . . . . 16 ((𝐹𝑘) ↾t (𝑆 (𝐹𝑘))) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆))
4643, 45syl6eq 2659 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4746unieqd 4376 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑘) ↾t ( (𝐹𝑘) ∩ 𝑆)))
4840, 47eqtr4d 2646 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ∩ 𝑆) = ((𝐹𝑘) ↾t 𝑆))
4948ixpeq2dva 7786 . . . . . . . . . . . 12 (𝜑X𝑘𝐴 ( (𝐹𝑘) ∩ 𝑆) = X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆))
50 ixpin 7796 . . . . . . . . . . . 12 X𝑘𝐴 ( (𝐹𝑘) ∩ 𝑆) = (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆)
51 nfcv 2750 . . . . . . . . . . . . . 14 𝑦 ((𝐹𝑘) ↾t 𝑆)
52 nfcv 2750 . . . . . . . . . . . . . . . 16 𝑘(𝐹𝑦)
53 nfcv 2750 . . . . . . . . . . . . . . . 16 𝑘t
54 nfcsb1v 3514 . . . . . . . . . . . . . . . 16 𝑘𝑦 / 𝑘𝑆
5552, 53, 54nfov 6552 . . . . . . . . . . . . . . 15 𝑘((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
5655nfuni 4372 . . . . . . . . . . . . . 14 𝑘 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
57 fveq2 6087 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (𝐹𝑘) = (𝐹𝑦))
58 csbeq1a 3507 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦𝑆 = 𝑦 / 𝑘𝑆)
5957, 58oveq12d 6544 . . . . . . . . . . . . . . 15 (𝑘 = 𝑦 → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6059unieqd 4376 . . . . . . . . . . . . . 14 (𝑘 = 𝑦 ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6151, 56, 60cbvixp 7788 . . . . . . . . . . . . 13 X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
62 ixpeq2 7785 . . . . . . . . . . . . . 14 (∀𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) → X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
63 ovex 6554 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) ∈ V
64 nfcv 2750 . . . . . . . . . . . . . . . . 17 𝑘𝑦
65 eqid 2609 . . . . . . . . . . . . . . . . 17 (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)) = (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))
6664, 55, 59, 65fvmptf 6193 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆) ∈ V) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6763, 66mpan2 702 . . . . . . . . . . . . . . 15 (𝑦𝐴 → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6867unieqd 4376 . . . . . . . . . . . . . 14 (𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆))
6962, 68mprg 2909 . . . . . . . . . . . . 13 X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = X𝑦𝐴 ((𝐹𝑦) ↾t 𝑦 / 𝑘𝑆)
7061, 69eqtr4i 2634 . . . . . . . . . . . 12 X𝑘𝐴 ((𝐹𝑘) ↾t 𝑆) = X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦)
7149, 50, 703eqtr3g 2666 . . . . . . . . . . 11 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆) = X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦))
72 eqid 2609 . . . . . . . . . . . . . 14 (∏t𝐹) = (∏t𝐹)
7372ptuni 21154 . . . . . . . . . . . . 13 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
743, 35, 73syl2anc 690 . . . . . . . . . . . 12 (𝜑X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
7574ineq1d 3774 . . . . . . . . . . 11 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ X𝑘𝐴 𝑆) = ( (∏t𝐹) ∩ X𝑘𝐴 𝑆))
76 resttop 20721 . . . . . . . . . . . . . 14 (((𝐹𝑘) ∈ Top ∧ 𝑆𝑊) → ((𝐹𝑘) ↾t 𝑆) ∈ Top)
7736, 13, 76syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ((𝐹𝑘) ↾t 𝑆) ∈ Top)
7877, 65fmptd 6276 . . . . . . . . . . . 12 (𝜑 → (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top)
79 eqid 2609 . . . . . . . . . . . . 13 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))
8079ptuni 21154 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
813, 78, 80syl2anc 690 . . . . . . . . . . 11 (𝜑X𝑦𝐴 ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑦) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
8271, 75, 813eqtr3d 2651 . . . . . . . . . 10 (𝜑 → ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
8382sneqd 4136 . . . . . . . . 9 (𝜑 → {( (∏t𝐹) ∩ X𝑘𝐴 𝑆)} = { (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))})
8434, 83syl5eq 2655 . . . . . . . 8 (𝜑 → ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) = { (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))})
85 vex 3175 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
8685elixp 7778 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤X𝑘𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆))
8786simprbi 478 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤X𝑘𝐴 𝑆 → ∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆)
88 nfcsb1v 3514 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝑢 / 𝑘𝑆
8988nfel2 2766 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝑤𝑢) ∈ 𝑢 / 𝑘𝑆
90 fveq2 6087 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑢 → (𝑤𝑘) = (𝑤𝑢))
91 csbeq1a 3507 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑢𝑆 = 𝑢 / 𝑘𝑆)
9290, 91eleq12d 2681 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑢 → ((𝑤𝑘) ∈ 𝑆 ↔ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9389, 92rspc 3275 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢𝐴 → (∀𝑘𝐴 (𝑤𝑘) ∈ 𝑆 → (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9487, 93syl5 33 . . . . . . . . . . . . . . . . . . . . 21 (𝑢𝐴 → (𝑤X𝑘𝐴 𝑆 → (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9594pm4.71d 663 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝐴 → (𝑤X𝑘𝐴 𝑆 ↔ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
9695anbi2d 735 . . . . . . . . . . . . . . . . . . 19 (𝑢𝐴 → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))))
97 an4 860 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
98 elin 3757 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆) ↔ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆))
9998anbi2i 725 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ ((𝑤𝑢) ∈ 𝑣 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)))
10097, 99bitr4i 265 . . . . . . . . . . . . . . . . . . 19 (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ (𝑤X𝑘𝐴 𝑆 ∧ (𝑤𝑢) ∈ 𝑢 / 𝑘𝑆)) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)))
10196, 100syl6bb 274 . . . . . . . . . . . . . . . . . 18 (𝑢𝐴 → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
102 elin 3757 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ↔ (𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆))
10382eleq2d 2672 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑤 ∈ ( (∏t𝐹) ∩ X𝑘𝐴 𝑆) ↔ 𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))))
104102, 103syl5bbr 272 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ↔ 𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))))
105104anbi1d 736 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑤 (∏t𝐹) ∧ 𝑤X𝑘𝐴 𝑆) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)) ↔ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
106101, 105sylan9bbr 732 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝐴) → (((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆) ↔ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))))
107106abbidv 2727 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝐴) → {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)} = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))})
108 eqid 2609 . . . . . . . . . . . . . . . . . . . 20 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) = (𝑤 (∏t𝐹) ↦ (𝑤𝑢))
109108mptpreima 5530 . . . . . . . . . . . . . . . . . . 19 ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) = {𝑤 (∏t𝐹) ∣ (𝑤𝑢) ∈ 𝑣}
110 df-rab 2904 . . . . . . . . . . . . . . . . . . 19 {𝑤 (∏t𝐹) ∣ (𝑤𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)}
111109, 110eqtr2i 2632 . . . . . . . . . . . . . . . . . 18 {𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)
112 abid2 2731 . . . . . . . . . . . . . . . . . 18 {𝑤𝑤X𝑘𝐴 𝑆} = X𝑘𝐴 𝑆
113111, 112ineq12i 3773 . . . . . . . . . . . . . . . . 17 ({𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} ∩ {𝑤𝑤X𝑘𝐴 𝑆}) = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)
114 inab 3853 . . . . . . . . . . . . . . . . 17 ({𝑤 ∣ (𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣)} ∩ {𝑤𝑤X𝑘𝐴 𝑆}) = {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)}
115113, 114eqtr3i 2633 . . . . . . . . . . . . . . . 16 (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) = {𝑤 ∣ ((𝑤 (∏t𝐹) ∧ (𝑤𝑢) ∈ 𝑣) ∧ 𝑤X𝑘𝐴 𝑆)}
116 eqid 2609 . . . . . . . . . . . . . . . . . 18 (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) = (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢))
117116mptpreima 5530 . . . . . . . . . . . . . . . . 17 ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = {𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∣ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)}
118 df-rab 2904 . . . . . . . . . . . . . . . . 17 {𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∣ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆)} = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))}
119117, 118eqtri 2631 . . . . . . . . . . . . . . . 16 ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = {𝑤 ∣ (𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ∧ (𝑤𝑢) ∈ (𝑣𝑢 / 𝑘𝑆))}
120107, 115, 1193eqtr4g 2668 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)))
121120eqeq2d 2619 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆))))
122121rexbidv 3033 . . . . . . . . . . . . 13 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆))))
123 ineq1 3768 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑦 → (𝑣𝑢 / 𝑘𝑆) = (𝑦𝑢 / 𝑘𝑆))
124123imaeq2d 5371 . . . . . . . . . . . . . . 15 (𝑣 = 𝑦 → ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
125124eqeq2d 2619 . . . . . . . . . . . . . 14 (𝑣 = 𝑦 → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
126125cbvrexv 3147 . . . . . . . . . . . . 13 (∃𝑣 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑣𝑢 / 𝑘𝑆)) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
127122, 126syl6bb 274 . . . . . . . . . . . 12 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
128 vex 3175 . . . . . . . . . . . . . . 15 𝑦 ∈ V
129128inex1 4721 . . . . . . . . . . . . . 14 (𝑦𝑢 / 𝑘𝑆) ∈ V
130129a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑢𝐴) ∧ 𝑦 ∈ (𝐹𝑢)) → (𝑦𝑢 / 𝑘𝑆) ∈ V)
131 ovex 6554 . . . . . . . . . . . . . . . . 17 ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ∈ V
132 nfcv 2750 . . . . . . . . . . . . . . . . . 18 𝑘𝑢
133 nfcv 2750 . . . . . . . . . . . . . . . . . . 19 𝑘(𝐹𝑢)
134133, 53, 88nfov 6552 . . . . . . . . . . . . . . . . . 18 𝑘((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆)
135 fveq2 6087 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝐹𝑘) = (𝐹𝑢))
136135, 91oveq12d 6544 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 → ((𝐹𝑘) ↾t 𝑆) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
137132, 134, 136, 65fvmptf 6193 . . . . . . . . . . . . . . . . 17 ((𝑢𝐴 ∧ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ∈ V) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
138131, 137mpan2 702 . . . . . . . . . . . . . . . 16 (𝑢𝐴 → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
139138adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) = ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆))
140139eleq2d 2672 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆)))
141 nfv 1829 . . . . . . . . . . . . . . . . 17 𝑘(𝜑𝑢𝐴)
142 nfcsb1v 3514 . . . . . . . . . . . . . . . . . 18 𝑘𝑢 / 𝑘𝑊
14388, 142nfel 2762 . . . . . . . . . . . . . . . . 17 𝑘𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊
144141, 143nfim 1812 . . . . . . . . . . . . . . . 16 𝑘((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)
145 eleq1 2675 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 → (𝑘𝐴𝑢𝐴))
146145anbi2d 735 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ((𝜑𝑘𝐴) ↔ (𝜑𝑢𝐴)))
147 csbeq1a 3507 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢𝑊 = 𝑢 / 𝑘𝑊)
14891, 147eleq12d 2681 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → (𝑆𝑊𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊))
149146, 148imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (((𝜑𝑘𝐴) → 𝑆𝑊) ↔ ((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)))
150144, 149, 13chvar 2249 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐴) → 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊)
151 elrest 15859 . . . . . . . . . . . . . . 15 (((𝐹𝑢) ∈ V ∧ 𝑢 / 𝑘𝑆𝑢 / 𝑘𝑊) → (𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
1524, 150, 151sylancr 693 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝐹𝑢) ↾t 𝑢 / 𝑘𝑆) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
153140, 152bitrd 266 . . . . . . . . . . . . 13 ((𝜑𝑢𝐴) → (𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑣 = (𝑦𝑢 / 𝑘𝑆)))
154 imaeq2 5367 . . . . . . . . . . . . . . 15 (𝑣 = (𝑦𝑢 / 𝑘𝑆) → ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆)))
155154eqeq2d 2619 . . . . . . . . . . . . . 14 (𝑣 = (𝑦𝑢 / 𝑘𝑆) → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
156155adantl 480 . . . . . . . . . . . . 13 (((𝜑𝑢𝐴) ∧ 𝑣 = (𝑦𝑢 / 𝑘𝑆)) → (𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ 𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
157130, 153, 156rexxfr2d 4803 . . . . . . . . . . . 12 ((𝜑𝑢𝐴) → (∃𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ (𝑦𝑢 / 𝑘𝑆))))
158127, 157bitr4d 269 . . . . . . . . . . 11 ((𝜑𝑢𝐴) → (∃𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
159158rexbidva 3030 . . . . . . . . . 10 (𝜑 → (∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
160159abbidv 2727 . . . . . . . . 9 (𝜑 → {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)} = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)})
161 eqid 2609 . . . . . . . . . . 11 (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))
162161rnmpt 5278 . . . . . . . . . 10 ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)}
163 nfre1 2987 . . . . . . . . . . 11 𝑥𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)
164 nfv 1829 . . . . . . . . . . 11 𝑦𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)
16527mptex 6367 . . . . . . . . . . . . . . . 16 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) ∈ V
166165cnvex 6983 . . . . . . . . . . . . . . 15 (𝑤 (∏t𝐹) ↦ (𝑤𝑢)) ∈ V
167 imaexg 6972 . . . . . . . . . . . . . . 15 ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) ∈ V → ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V)
168166, 167ax-mp 5 . . . . . . . . . . . . . 14 ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V
169168rgen2w 2908 . . . . . . . . . . . . 13 𝑢𝐴𝑣 ∈ (𝐹𝑢)((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V
170 ineq1 3768 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) → (𝑥X𝑘𝐴 𝑆) = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆))
171170eqeq2d 2619 . . . . . . . . . . . . . 14 (𝑥 = ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) → (𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ 𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
1726, 171rexrnmpt2 6651 . . . . . . . . . . . . 13 (∀𝑢𝐴𝑣 ∈ (𝐹𝑢)((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∈ V → (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
173169, 172ax-mp 5 . . . . . . . . . . . 12 (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆))
174 eqeq1 2613 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ 𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
1751742rexbidv 3038 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑦 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
176173, 175syl5bb 270 . . . . . . . . . . 11 (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆) ↔ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)))
177163, 164, 176cbvab 2732 . . . . . . . . . 10 {𝑦 ∣ ∃𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))𝑦 = (𝑥X𝑘𝐴 𝑆)} = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)}
178162, 177eqtri 2631 . . . . . . . . 9 ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ (𝐹𝑢)𝑥 = (((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣) ∩ X𝑘𝐴 𝑆)}
179 eqid 2609 . . . . . . . . . 10 (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)) = (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))
180179rnmpt2 6645 . . . . . . . . 9 ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢𝐴𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢)𝑥 = ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)}
181160, 178, 1803eqtr4g 2668 . . . . . . . 8 (𝜑 → ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆)) = ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))
18284, 181uneq12d 3729 . . . . . . 7 (𝜑 → (ran (𝑥 ∈ { (∏t𝐹)} ↦ (𝑥X𝑘𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)) ↦ (𝑥X𝑘𝐴 𝑆))) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
18322, 182syl5eq 2655 . . . . . 6 (𝜑 → ran (𝑥 ∈ ({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↦ (𝑥X𝑘𝐴 𝑆)) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
18418, 183eqtrd 2643 . . . . 5 (𝜑 → (({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆) = ({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))
185184fveq2d 6091 . . . 4 (𝜑 → (fi‘(({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))) ↾t X𝑘𝐴 𝑆)) = (fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))))
1861, 185syl5eqr 2657 . . 3 (𝜑 → ((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆) = (fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣)))))
187186fveq2d 6091 . 2 (𝜑 → (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
188 eqid 2609 . . . . . 6 (∏t𝐹) = (∏t𝐹)
18972, 188, 6ptval2 21161 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) = (topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))))
1903, 35, 189syl2anc 690 . . . 4 (𝜑 → (∏t𝐹) = (topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))))
191190oveq1d 6541 . . 3 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = ((topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))) ↾t X𝑘𝐴 𝑆))
192 fvex 6097 . . . 4 (fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ∈ V
193 tgrest 20720 . . . 4 (((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ∈ V ∧ X𝑘𝐴 𝑆 ∈ V) → (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)) = ((topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))) ↾t X𝑘𝐴 𝑆))
194192, 16, 193sylancr 693 . . 3 (𝜑 → (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)) = ((topGen‘(fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣))))) ↾t X𝑘𝐴 𝑆))
195191, 194eqtr4d 2646 . 2 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = (topGen‘((fi‘({ (∏t𝐹)} ∪ ran (𝑢𝐴, 𝑣 ∈ (𝐹𝑢) ↦ ((𝑤 (∏t𝐹) ↦ (𝑤𝑢)) “ 𝑣)))) ↾t X𝑘𝐴 𝑆)))
196 eqid 2609 . . . 4 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))
19779, 196, 179ptval2 21161 . . 3 ((𝐴𝑉 ∧ (𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)):𝐴⟶Top) → (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
1983, 78, 197syl2anc 690 . 2 (𝜑 → (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) = (topGen‘(fi‘({ (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆)))} ∪ ran (𝑢𝐴, 𝑣 ∈ ((𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))‘𝑢) ↦ ((𝑤 (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))) ↦ (𝑤𝑢)) “ 𝑣))))))
199187, 195, 1983eqtr4d 2653 1 (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  {cab 2595  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  csb 3498  cun 3537  cin 3538  wss 3539  {csn 4124  cop 4130   cuni 4366  cmpt 4637  ccnv 5026  ran crn 5028  cima 5030   Fn wfn 5784  wf 5785  cfv 5789  (class class class)co 6526  cmpt2 6528  Xcixp 7771  ficfi 8176  t crest 15852  topGenctg 15869  tcpt 15870  Topctop 20464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-ixp 7772  df-en 7819  df-dom 7820  df-fin 7822  df-fi 8177  df-rest 15854  df-topgen 15875  df-pt 15876  df-top 20468  df-bases 20469  df-topon 20470
This theorem is referenced by:  poimirlem30  32392
  Copyright terms: Public domain W3C validator