Theorem ptrest 35785

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.

Step	Hyp	Ref	Expression
1		firest 17152	. . . 4 ⊢ (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆)) = ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)
2		snex 5355	. . . . . . . 8 ⊢ {∪ (∏t‘𝐹)} ∈ V
3		ptrest.0	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		fvex 6796	. . . . . . . . . . 11 ⊢ (𝐹‘𝑢) ∈ V
5	4	rgenw 3077	. . . . . . . . . 10 ⊢ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V
6		eqid 2739	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))
7	6	mpoexxg 7925	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V) → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
8	3, 5, 7	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
9		rnexg 7760	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
10	8, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
11		unexg 7608	. . . . . . . 8 ⊢ (({∪ (∏t‘𝐹)} ∈ V ∧ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V)
12	2, 10, 11	sylancr 587	. . . . . . 7 ⊢ (𝜑 → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V)
13		ptrest.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊)
14	13	ralrimiva 3104	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊)
15		ixpexg 8719	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
17		restval 17146	. . . . . . 7 ⊢ ((({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V ∧ X𝑘 ∈ 𝐴 𝑆 ∈ V) → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
18	12, 16, 17	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
19		mptun 6588	. . . . . . . . 9 ⊢ (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
20	19	rneqi 5849	. . . . . . . 8 ⊢ ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
21		rnun 6054	. . . . . . . 8 ⊢ ran ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
22	20, 21	eqtri 2767	. . . . . . 7 ⊢ ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
23		elsni 4579	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → 𝑥 = ∪ (∏t‘𝐹))
24	23	ineq1d 4146	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
25	24	mpteq2ia 5178	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
26		fvex 6796	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) ∈ V
27	26	uniex 7603	. . . . . . . . . . . . 13 ⊢ ∪ (∏t‘𝐹) ∈ V
28	27	inex1 5242	. . . . . . . . . . . . 13 ⊢ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V
29		fmptsn 7048	. . . . . . . . . . . . 13 ⊢ ((∪ (∏t‘𝐹) ∈ V ∧ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V) → {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)))
30	27, 28, 29	mp2an 689	. . . . . . . . . . . 12 ⊢ {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
31	25, 30	eqtr4i 2770	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
32	31	rneqi 5849	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
33	27	rnsnop 6132	. . . . . . . . . 10 ⊢ ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
34	32, 33	eqtri 2767	. . . . . . . . 9 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
35		ptrest.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝐴⟶Top)
36	35	ffvelrnda 6970	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Top)
37		inss1 4163	. . . . . . . . . . . . . . 15 ⊢ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)
38		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
39	38	restuni 22322	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑘) ∈ Top ∧ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
40	36, 37, 39	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
41		fvex 6796	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑘) ∈ V
42	38	restin 22326	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑘) ∈ V ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
43	41, 13, 42	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
44		incom 4136	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ ∪ (𝐹‘𝑘)) = (∪ (𝐹‘𝑘) ∩ 𝑆)
45	44	oveq2i 7295	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))
46	43, 45	eqtrdi 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
47	46	unieqd 4854	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
48	40, 47	eqtr4d 2782	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t 𝑆))
49	48	ixpeq2dva 8709	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆))
50		ixpin 8720	. . . . . . . . . . . 12 ⊢ X𝑘 ∈ 𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆)
51		nfcv 2908	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∪ ((𝐹‘𝑘) ↾t 𝑆)
52		nfcv 2908	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(𝐹‘𝑦)
53		nfcv 2908	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘 ↾t
54		nfcsb1v 3858	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝑆
55	52, 53, 54	nfov 7314	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
56	55	nfuni 4847	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
57		fveq2 6783	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦))
58		csbeq1a 3847	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → 𝑆 = ⦋𝑦 / 𝑘⦌𝑆)
59	57, 58	oveq12d 7302	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑦 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
60	59	unieqd 4854	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑦 → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
61	51, 56, 60	cbvixp 8711	. . . . . . . . . . . . 13 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
62		ixpeq2 8708	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
63		ovex 7317	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V
64		nfcv 2908	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘𝑦
65		eqid 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))
66	64, 55, 59, 65	fvmptf 6905	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
67	63, 66	mpan2 688	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
68	67	unieqd 4854	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
69	62, 68	mprg 3079	. . . . . . . . . . . . 13 ⊢ X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
70	61, 69	eqtr4i 2770	. . . . . . . . . . . 12 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦)
71	49, 50, 70	3eqtr3g 2802	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦))
72		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) = (∏t‘𝐹)
73	72	ptuni 22754	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
74	3, 35, 73	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
75	74	ineq1d 4146	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
76		resttop 22320	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑘) ∈ Top ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
77	36, 13, 76	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
78	77	fmpttd 6998	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top)
79		eqid 2739	. . . . . . . . . . . . 13 ⊢ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
80	79	ptuni 22754	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
81	3, 78, 80	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
82	71, 75, 81	3eqtr3d 2787	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
83	82	sneqd 4574	. . . . . . . . 9 ⊢ (𝜑 → {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)} = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
84	34, 83	eqtrid 2791	. . . . . . . 8 ⊢ (𝜑 → ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
85		vex 3437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑤 ∈ V
86	85	elixp 8701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆))
87	86	simprbi 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆)
88		nfcsb1v 3858	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆
89	88	nfel2 2926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆
90		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → (𝑤‘𝑘) = (𝑤‘𝑢))
91		csbeq1a 3847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → 𝑆 = ⦋𝑢 / 𝑘⦌𝑆)
92	90, 91	eleq12d 2834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑢 → ((𝑤‘𝑘) ∈ 𝑆 ↔ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
93	89, 92	rspc 3550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
94	87, 93	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
95	94	pm4.71d 562	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
96	95	anbi2d 629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))))
97		an4 653	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
98		elin 3904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) ↔ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
99	98	anbi2i 623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
100	97, 99	bitr4i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
101	96, 100	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
102		elin 3904	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆))
103	82	eleq2d 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
104	102, 103	bitr3id 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
105	104	anbi1d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
106	101, 105	sylan9bbr 511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
107	106	abbidv 2808	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))})
108		eqid 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢))
109	108	mptpreima 6146	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) = {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣}
110		df-rab 3074	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)}
111	109, 110	eqtr2i 2768	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)
112		abid2 2883	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆} = X𝑘 ∈ 𝐴 𝑆
113	111, 112	ineq12i 4145	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
114		inab 4234	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
115	113, 114	eqtr3i 2769	. . . . . . . . . . . . . . . 16 ⊢ ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
116		eqid 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢))
117	116	mptpreima 6146	. . . . . . . . . . . . . . . . 17 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)}
118		df-rab 3074	. . . . . . . . . . . . . . . . 17 ⊢ {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
119	117, 118	eqtri 2767	. . . . . . . . . . . . . . . 16 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
120	107, 115, 119	3eqtr4g 2804	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
121	120	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
122	121	rexbidv 3227	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
123		ineq1 4140	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑦 → (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))
124	123	imaeq2d 5972	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
125	124	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
126	125	cbvrexvw 3385	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
127	122, 126	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
128		vex 3437	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
129	128	inex1 5242	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑦 ∈ (𝐹‘𝑢)) → (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V)
131		ovex 7317	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V
132		nfcv 2908	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘𝑢
133		nfcv 2908	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘(𝐹‘𝑢)
134	133, 53, 88	nfov 7314	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)
135		fveq2 6783	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (𝐹‘𝑘) = (𝐹‘𝑢))
136	135, 91	oveq12d 7302	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
137	132, 134, 136, 65	fvmptf 6905	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝐴 ∧ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
138	131, 137	mpan2 688	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
139	138	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
140	139	eleq2d 2825	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)))
141		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑢 ∈ 𝐴)
142		nfcsb1v 3858	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑊
143	88, 142	nfel 2922	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊
144	141, 143	nfim 1900	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
145		eleq1w 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → (𝑘 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
146	145	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴)))
147		csbeq1a 3847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → 𝑊 = ⦋𝑢 / 𝑘⦌𝑊)
148	91, 147	eleq12d 2834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (𝑆 ∈ 𝑊 ↔ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊))
149	146, 148	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)))
150	144, 149, 13	chvarfv 2234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
151		elrest 17147	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑢) ∈ V ∧ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
152	4, 150, 151	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
153	140, 152	bitrd 278	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
154		imaeq2 5968	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
155	154	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
156	155	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)) → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
157	130, 153, 156	rexxfr2d 5335	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
158	127, 157	bitr4d 281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
159	158	rexbidva 3226	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
160	159	abbidv 2808	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)})
161		eqid 2739	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))
162	161	rnmpt 5867	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)}
163		nfre1 3240	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)
164		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
165	27	mptex 7108	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
166	165	cnvex 7781	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
167	166	imaex 7772	. . . . . . . . . . . . . 14 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
168	167	rgen2w 3078	. . . . . . . . . . . . 13 ⊢ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
169		ineq1 4140	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))
170	169	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
171	6, 170	rexrnmpo 7422	. . . . . . . . . . . . 13 ⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
172	168, 171	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))
173		eqeq1 2743	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
174	173	2rexbidv 3230	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
175	172, 174	syl5bb 283	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
176	163, 164, 175	cbvabw 2813	. . . . . . . . . 10 ⊢ {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
177	162, 176	eqtri 2767	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
178		eqid 2739	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))
179	178	rnmpo 7416	. . . . . . . . 9 ⊢ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)}
180	160, 177, 179	3eqtr4g 2804	. . . . . . . 8 ⊢ (𝜑 → ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
181	84, 180	uneq12d 4099	. . . . . . 7 ⊢ (𝜑 → (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
182	22, 181	eqtrid 2791	. . . . . 6 ⊢ (𝜑 → ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
183	18, 182	eqtrd 2779	. . . . 5 ⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
184	183	fveq2d 6787	. . . 4 ⊢ (𝜑 → (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆)) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
185	1, 184	eqtr3id 2793	. . 3 ⊢ (𝜑 → ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
186	185	fveq2d 6787	. 2 ⊢ (𝜑 → (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
187		eqid 2739	. . . . . 6 ⊢ ∪ (∏t‘𝐹) = ∪ (∏t‘𝐹)
188	72, 187, 6	ptval2 22761	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
189	3, 35, 188	syl2anc 584	. . . 4 ⊢ (𝜑 → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
190	189	oveq1d 7299	. . 3 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈ 𝐴 𝑆))
191		fvex 6796	. . . 4 ⊢ (fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ∈ V
192		tgrest 22319	. . . 4 ⊢ (((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ∈ V ∧ X𝑘 ∈ 𝐴 𝑆 ∈ V) → (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈ 𝐴 𝑆))
193	191, 16, 192	sylancr 587	. . 3 ⊢ (𝜑 → (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈ 𝐴 𝑆))
194	190, 193	eqtr4d 2782	. 2 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)))
195		eqid 2739	. . . 4 ⊢ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
196	79, 195, 178	ptval2 22761	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
197	3, 78, 196	syl2anc 584	. 2 ⊢ (𝜑 → (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
198	186, 194, 197	3eqtr4d 2789	1 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {cab 2716  ∀wral 3065  ∃wrex 3066  {crab 3069  Vcvv 3433  ⦋csb 3833   ∪ cun 3886   ∩ cin 3887   ⊆ wss 3888  {csn 4562  ⟨cop 4568  ∪ cuni 4840   ↦ cmpt 5158  ^◡ccnv 5589  ran crn 5591   “ cima 5593   Fn wfn 6432  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284   ∈ cmpo 7286  Xcixp 8694  ficfi 9178   ↾_t crest 17140  topGenctg 17157  ∏_tcpt 17158  Topctop 22051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-1o 8306  df-er 8507  df-ixp 8695  df-en 8743  df-dom 8744  df-fin 8746  df-fi 9179  df-rest 17142  df-topgen 17163  df-pt 17164  df-top 22052  df-topon 22069  df-bases 22105

This theorem is referenced by:  poimirlem30  35816