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.

Step	Hyp	Ref	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
5	4	rgenw 3065	. . . . . . . . . 10 ⊢ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V
6		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))
7	6	mpoexxg 8100	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V) → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
8	3, 5, 7	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
9		rnexg 7924	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
10	8, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
11		unexg 7763	. . . . . . . 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 3146	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊)
15		ixpexg 8962	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
17		restval 17471	. . . . . . 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 6714	. . . . . . . . 9 ⊢ (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
20	19	rneqi 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𝑘 ∈ 𝐴 𝑆)))
22	20, 21	eqtri 2765	. . . . . . 7 ⊢ ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
23		elsni 4643	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → 𝑥 = ∪ (∏t‘𝐹))
24	23	ineq1d 4219	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
25	24	mpteq2ia 5245	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
26		fvex 6919	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) ∈ V
27	26	uniex 7761	. . . . . . . . . . . . 13 ⊢ ∪ (∏t‘𝐹) ∈ V
28	27	inex1 5317	. . . . . . . . . . . . 13 ⊢ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V
29		fmptsn 7187	. . . . . . . . . . . . 13 ⊢ ((∪ (∏t‘𝐹) ∈ V ∧ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V) → {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)))
30	27, 28, 29	mp2an 692	. . . . . . . . . . . 12 ⊢ {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
31	25, 30	eqtr4i 2768	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
32	31	rneqi 5948	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
33	27	rnsnop 6244	. . . . . . . . . 10 ⊢ ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
34	32, 33	eqtri 2765	. . . . . . . . 9 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
35		ptrest.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝐴⟶Top)
36	35	ffvelcdmda 7104	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Top)
37		inss1 4237	. . . . . . . . . . . . . . 15 ⊢ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)
38		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
39	38	restuni 23170	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑘) ∈ Top ∧ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
40	36, 37, 39	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
41		fvex 6919	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑘) ∈ V
42	38	restin 23174	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑘) ∈ V ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
43	41, 13, 42	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
44		incom 4209	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ ∪ (𝐹‘𝑘)) = (∪ (𝐹‘𝑘) ∩ 𝑆)
45	44	oveq2i 7442	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))
46	43, 45	eqtrdi 2793	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
47	46	unieqd 4920	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
48	40, 47	eqtr4d 2780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t 𝑆))
49	48	ixpeq2dva 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 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝑆
55	52, 53, 54	nfov 7461	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
56	55	nfuni 4914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
57		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦))
58		csbeq1a 3913	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → 𝑆 = ⦋𝑦 / 𝑘⦌𝑆)
59	57, 58	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑦 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
60	59	unieqd 4920	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑦 → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
61	51, 56, 60	cbvixp 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 𝑆))
66	64, 55, 59, 65	fvmptf 7037	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
67	63, 66	mpan2 691	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
68	67	unieqd 4920	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
69	62, 68	mprg 3067	. . . . . . . . . . . . 13 ⊢ X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
70	61, 69	eqtr4i 2768	. . . . . . . . . . . 12 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦)
71	49, 50, 70	3eqtr3g 2800	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦))
72		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) = (∏t‘𝐹)
73	72	ptuni 23602	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
74	3, 35, 73	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
75	74	ineq1d 4219	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
76		resttop 23168	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑘) ∈ Top ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
77	36, 13, 76	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
78	77	fmpttd 7135	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top)
79		eqid 2737	. . . . . . . . . . . . 13 ⊢ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
80	79	ptuni 23602	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
81	3, 78, 80	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
82	71, 75, 81	3eqtr3d 2785	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
83	82	sneqd 4638	. . . . . . . . 9 ⊢ (𝜑 → {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)} = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
84	34, 83	eqtrid 2789	. . . . . . . 8 ⊢ (𝜑 → ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
85		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑤 ∈ V
86	85	elixp 8944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆))
87	86	simprbi 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆)
88		nfcsb1v 3923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆
89	88	nfel2 2924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆
90		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → (𝑤‘𝑘) = (𝑤‘𝑢))
91		csbeq1a 3913	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → 𝑆 = ⦋𝑢 / 𝑘⦌𝑆)
92	90, 91	eleq12d 2835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑢 → ((𝑤‘𝑘) ∈ 𝑆 ↔ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
93	89, 92	rspc 3610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
94	87, 93	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
95	94	pm4.71d 561	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
96	95	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))))
97		an4 656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
98		elin 3967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) ↔ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
99	98	anbi2i 623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
100	97, 99	bitr4i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
101	96, 100	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
102		elin 3967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆))
103	82	eleq2d 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
104	102, 103	bitr3id 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
105	104	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
106	101, 105	sylan9bbr 510	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
107	106	abbidv 2808	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))})
108		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢))
109	108	mptpreima 6258	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) = {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣}
110		df-rab 3437	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)}
111	109, 110	eqtr2i 2766	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)
112		abid2 2879	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆} = X𝑘 ∈ 𝐴 𝑆
113	111, 112	ineq12i 4218	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
114		inab 4309	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
115	113, 114	eqtr3i 2767	. . . . . . . . . . . . . . . 16 ⊢ ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
116		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢))
117	116	mptpreima 6258	. . . . . . . . . . . . . . . . 17 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)}
118		df-rab 3437	. . . . . . . . . . . . . . . . 17 ⊢ {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
119	117, 118	eqtri 2765	. . . . . . . . . . . . . . . 16 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
120	107, 115, 119	3eqtr4g 2802	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
121	120	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
122	121	rexbidv 3179	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
123		ineq1 4213	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑦 → (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))
124	123	imaeq2d 6078	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
125	124	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
126	125	cbvrexvw 3238	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
127	122, 126	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
128		vex 3484	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
129	128	inex1 5317	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑦 ∈ (𝐹‘𝑢)) → (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V)
131		ovex 7464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V
132		nfcv 2905	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘𝑢
133		nfcv 2905	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘(𝐹‘𝑢)
134	133, 53, 88	nfov 7461	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)
135		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (𝐹‘𝑘) = (𝐹‘𝑢))
136	135, 91	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
137	132, 134, 136, 65	fvmptf 7037	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝐴 ∧ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
138	131, 137	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
139	138	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
140	139	eleq2d 2827	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)))
141		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑢 ∈ 𝐴)
142		nfcsb1v 3923	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑊
143	88, 142	nfel 2920	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊
144	141, 143	nfim 1896	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
145		eleq1w 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → (𝑘 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
146	145	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴)))
147		csbeq1a 3913	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → 𝑊 = ⦋𝑢 / 𝑘⦌𝑊)
148	91, 147	eleq12d 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (𝑆 ∈ 𝑊 ↔ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊))
149	146, 148	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)))
150	144, 149, 13	chvarfv 2240	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
151		elrest 17472	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑢) ∈ V ∧ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
152	4, 150, 151	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
153	140, 152	bitrd 279	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
154		imaeq2 6074	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
155	154	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
156	155	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)) → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
157	130, 153, 156	rexxfr2d 5411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
158	127, 157	bitr4d 282	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
159	158	rexbidva 3177	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
160	159	abbidv 2808	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)})
161		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))
162	161	rnmpt 5968	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)}
163		nfre1 3285	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)
164		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
165	27	mptex 7243	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
166	165	cnvex 7947	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
167	166	imaex 7936	. . . . . . . . . . . . . 14 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
168	167	rgen2w 3066	. . . . . . . . . . . . 13 ⊢ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
169		ineq1 4213	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))
170	169	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
171	6, 170	rexrnmpo 7573	. . . . . . . . . . . . 13 ⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
172	168, 171	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))
173		eqeq1 2741	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
174	173	2rexbidv 3222	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
175	172, 174	bitrid 283	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
176	163, 164, 175	cbvabw 2813	. . . . . . . . . 10 ⊢ {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
177	162, 176	eqtri 2765	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
178		eqid 2737	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))
179	178	rnmpo 7566	. . . . . . . . 9 ⊢ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)}
180	160, 177, 179	3eqtr4g 2802	. . . . . . . 8 ⊢ (𝜑 → ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
181	84, 180	uneq12d 4169	. . . . . . 7 ⊢ (𝜑 → (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
182	22, 181	eqtrid 2789	. . . . . 6 ⊢ (𝜑 → ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
183	18, 182	eqtrd 2777	. . . . 5 ⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
184	183	fveq2d 6910	. . . 4 ⊢ (𝜑 → (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆)) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
185	1, 184	eqtr3id 2791	. . 3 ⊢ (𝜑 → ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
186	185	fveq2d 6910	. 2 ⊢ (𝜑 → (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
187		eqid 2737	. . . . . 6 ⊢ ∪ (∏t‘𝐹) = ∪ (∏t‘𝐹)
188	72, 187, 6	ptval2 23609	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
189	3, 35, 188	syl2anc 584	. . . 4 ⊢ (𝜑 → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
190	189	oveq1d 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𝑘 ∈ 𝐴 𝑆))
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 2780	. 2 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)))
195		eqid 2737	. . . 4 ⊢ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
196	79, 195, 178	ptval2 23609	. . 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 2787	1 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))

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