Theorem ptrest 37986

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 17386	. . . 4 ⊢ (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆)) = ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)
2		snex 5368	. . . . . . . 8 ⊢ {∪ (∏t‘𝐹)} ∈ V
3		ptrest.0	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		fvex 6840	. . . . . . . . . . 11 ⊢ (𝐹‘𝑢) ∈ V
5	4	rgenw 3057	. . . . . . . . . 10 ⊢ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V
6		eqid 2739	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))
7	6	mpoexxg 8017	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V) → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
8	3, 5, 7	sylancl 592	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
9		rnexg 7842	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
10	8, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
11		unexg 7686	. . . . . . . 8 ⊢ (({∪ (∏t‘𝐹)} ∈ V ∧ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V)
12	2, 10, 11	sylancr 593	. . . . . . 7 ⊢ (𝜑 → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V)
13		ptrest.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊)
14	13	ralrimiva 3131	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊)
15		ixpexg 8860	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
17		restval 17380	. . . . . . 7 ⊢ ((({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V ∧ X𝑘 ∈ 𝐴 𝑆 ∈ V) → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
18	12, 16, 17	syl2anc 590	. . . . . 6 ⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
19		mptun 6631	. . . . . . . . 9 ⊢ (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
20	19	rneqi 5879	. . . . . . . 8 ⊢ ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
21		rnun 6096	. . . . . . . 8 ⊢ ran ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
22	20, 21	eqtri 2762	. . . . . . 7 ⊢ ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
23		elsni 4572	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → 𝑥 = ∪ (∏t‘𝐹))
24	23	ineq1d 4148	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
25	24	mpteq2ia 5167	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
26		fvex 6840	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) ∈ V
27	26	uniex 7684	. . . . . . . . . . . . 13 ⊢ ∪ (∏t‘𝐹) ∈ V
28	27	inex1 5245	. . . . . . . . . . . . 13 ⊢ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V
29		fmptsn 7111	. . . . . . . . . . . . 13 ⊢ ((∪ (∏t‘𝐹) ∈ V ∧ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V) → {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)))
30	27, 28, 29	mp2an 698	. . . . . . . . . . . 12 ⊢ {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
31	25, 30	eqtr4i 2765	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
32	31	rneqi 5879	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
33	27	rnsnop 6175	. . . . . . . . . 10 ⊢ ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
34	32, 33	eqtri 2762	. . . . . . . . 9 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
35		ptrest.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝐴⟶Top)
36	35	ffvelcdmda 7025	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Top)
37		inss1 4165	. . . . . . . . . . . . . . 15 ⊢ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)
38		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
39	38	restuni 23145	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑘) ∈ Top ∧ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
40	36, 37, 39	sylancl 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
41		fvex 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑘) ∈ V
42	38	restin 23149	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑘) ∈ V ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
43	41, 13, 42	sylancr 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
44		incom 4138	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ ∪ (𝐹‘𝑘)) = (∪ (𝐹‘𝑘) ∩ 𝑆)
45	44	oveq2i 7367	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))
46	43, 45	eqtrdi 2790	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
47	46	unieqd 4851	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
48	40, 47	eqtr4d 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t 𝑆))
49	48	ixpeq2dva 8850	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆))
50		ixpin 8861	. . . . . . . . . . . 12 ⊢ X𝑘 ∈ 𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆)
51		nfcv 2901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∪ ((𝐹‘𝑘) ↾t 𝑆)
52		nfcv 2901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(𝐹‘𝑦)
53		nfcv 2901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘 ↾t
54		nfcsb1v 3855	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝑆
55	52, 53, 54	nfov 7386	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
56	55	nfuni 4845	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
57		fveq2 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦))
58		csbeq1a 3845	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → 𝑆 = ⦋𝑦 / 𝑘⦌𝑆)
59	57, 58	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑦 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
60	59	unieqd 4851	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑦 → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
61	51, 56, 60	cbvixp 8852	. . . . . . . . . . . . 13 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
62		ixpeq2 8849	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
63		ovex 7389	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V
64		nfcv 2901	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘𝑦
65		eqid 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))
66	64, 55, 59, 65	fvmptf 6957	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
67	63, 66	mpan2 697	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
68	67	unieqd 4851	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
69	62, 68	mprg 3059	. . . . . . . . . . . . 13 ⊢ X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
70	61, 69	eqtr4i 2765	. . . . . . . . . . . 12 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦)
71	49, 50, 70	3eqtr3g 2797	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦))
72		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) = (∏t‘𝐹)
73	72	ptuni 23577	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
74	3, 35, 73	syl2anc 590	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
75	74	ineq1d 4148	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
76		resttop 23143	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑘) ∈ Top ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
77	36, 13, 76	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
78	77	fmpttd 7056	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top)
79		eqid 2739	. . . . . . . . . . . . 13 ⊢ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
80	79	ptuni 23577	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
81	3, 78, 80	syl2anc 590	. . . . . . . . . . 11 ⊢ (𝜑 → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
82	71, 75, 81	3eqtr3d 2782	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
83	82	sneqd 4567	. . . . . . . . 9 ⊢ (𝜑 → {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)} = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
84	34, 83	eqtrid 2786	. . . . . . . 8 ⊢ (𝜑 → ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
85		vex 3435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑤 ∈ V
86	85	elixp 8842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆))
87	86	simprbi 498	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆)
88		nfcsb1v 3855	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆
89	88	nfel2 2919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆
90		fveq2 6827	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → (𝑤‘𝑘) = (𝑤‘𝑢))
91		csbeq1a 3845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → 𝑆 = ⦋𝑢 / 𝑘⦌𝑆)
92	90, 91	eleq12d 2833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑢 → ((𝑤‘𝑘) ∈ 𝑆 ↔ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
93	89, 92	rspc 3548	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
94	87, 93	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
95	94	pm4.71d 566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
96	95	anbi2d 636	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))))
97		an4 662	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
98		elin 3899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) ↔ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
99	98	anbi2i 629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
100	97, 99	bitr4i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
101	96, 100	bitrdi 288	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
102		elin 3899	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆))
103	82	eleq2d 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
104	102, 103	bitr3id 286	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
105	104	anbi1d 637	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
106	101, 105	sylan9bbr 515	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
107	106	abbidv 2805	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))})
108		eqid 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢))
109	108	mptpreima 6189	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) = {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣}
110		df-rab 3392	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)}
111	109, 110	eqtr2i 2763	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)
112		abid2 2876	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆} = X𝑘 ∈ 𝐴 𝑆
113	111, 112	ineq12i 4147	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
114		inab 4237	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
115	113, 114	eqtr3i 2764	. . . . . . . . . . . . . . . 16 ⊢ ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
116		eqid 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢))
117	116	mptpreima 6189	. . . . . . . . . . . . . . . . 17 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)}
118		df-rab 3392	. . . . . . . . . . . . . . . . 17 ⊢ {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
119	117, 118	eqtri 2762	. . . . . . . . . . . . . . . 16 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
120	107, 115, 119	3eqtr4g 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
121	120	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
122	121	rexbidv 3163	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
123		ineq1 4142	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑦 → (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))
124	123	imaeq2d 6012	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
125	124	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
126	125	cbvrexvw 3218	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
127	122, 126	bitrdi 288	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
128		vex 3435	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
129	128	inex1 5245	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑦 ∈ (𝐹‘𝑢)) → (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V)
131		ovex 7389	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V
132		nfcv 2901	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘𝑢
133		nfcv 2901	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘(𝐹‘𝑢)
134	133, 53, 88	nfov 7386	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)
135		fveq2 6827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (𝐹‘𝑘) = (𝐹‘𝑢))
136	135, 91	oveq12d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
137	132, 134, 136, 65	fvmptf 6957	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝐴 ∧ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
138	131, 137	mpan2 697	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
139	138	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
140	139	eleq2d 2825	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)))
141		nfv 1921	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑢 ∈ 𝐴)
142		nfcsb1v 3855	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑊
143	88, 142	nfel 2915	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊
144	141, 143	nfim 1903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
145		eleq1w 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → (𝑘 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
146	145	anbi2d 636	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴)))
147		csbeq1a 3845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → 𝑊 = ⦋𝑢 / 𝑘⦌𝑊)
148	91, 147	eleq12d 2833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (𝑆 ∈ 𝑊 ↔ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊))
149	146, 148	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)))
150	144, 149, 13	chvarfv 2252	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
151		elrest 17381	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑢) ∈ V ∧ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
152	4, 150, 151	sylancr 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
153	140, 152	bitrd 280	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
154		imaeq2 6008	. . . . . . . . . . . . . . 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 5340	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
158	127, 157	bitr4d 283	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
159	158	rexbidva 3161	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
160	159	abbidv 2805	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)})
161		eqid 2739	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))
162	161	rnmpt 5899	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)}
163		nfre1 3264	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)
164		nfv 1921	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
165	27	mptex 7167	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
166	165	cnvex 7865	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
167	166	imaex 7854	. . . . . . . . . . . . . 14 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
168	167	rgen2w 3058	. . . . . . . . . . . . 13 ⊢ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
169		ineq1 4142	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))
170	169	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
171	6, 170	rexrnmpo 7496	. . . . . . . . . . . . 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 3204	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
175	172, 174	bitrid 284	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
176	163, 164, 175	cbvabw 2810	. . . . . . . . . 10 ⊢ {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
177	162, 176	eqtri 2762	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
178		eqid 2739	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))
179	178	rnmpo 7489	. . . . . . . . 9 ⊢ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)}
180	160, 177, 179	3eqtr4g 2799	. . . . . . . 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 2786	. . . . . 6 ⊢ (𝜑 → ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
183	18, 182	eqtrd 2774	. . . . 5 ⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
184	183	fveq2d 6831	. . . 4 ⊢ (𝜑 → (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆)) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
185	1, 184	eqtr3id 2788	. . 3 ⊢ (𝜑 → ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
186	185	fveq2d 6831	. 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 23584	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
189	3, 35, 188	syl2anc 590	. . . 4 ⊢ (𝜑 → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
190	189	oveq1d 7371	. . 3 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈ 𝐴 𝑆))
191		fvex 6840	. . . 4 ⊢ (fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ∈ V
192		tgrest 23142	. . . 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 593	. . 3 ⊢ (𝜑 → (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈ 𝐴 𝑆))
194	190, 193	eqtr4d 2777	. 2 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)))
195		eqid 2739	. . . 4 ⊢ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
196	79, 195, 178	ptval2 23584	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
197	3, 78, 196	syl2anc 590	. 2 ⊢ (𝜑 → (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
198	186, 194, 197	3eqtr4d 2784	1 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2717  ∀wral 3053  ∃wrex 3063  {crab 3391  Vcvv 3431  ⦋csb 3831   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  {csn 4555  ⟨cop 4561  ∪ cuni 4838   ↦ cmpt 5153  ^◡ccnv 5617  ran crn 5619   “ cima 5621   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356   ∈ cmpo 7358  Xcixp 8835  ficfi 9313   ↾_t crest 17374  topGenctg 17391  ∏_tcpt 17392  Topctop 22876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-iin 4924  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-1o 8395  df-2o 8396  df-ixp 8836  df-en 8884  df-dom 8885  df-fin 8887  df-fi 9314  df-rest 17376  df-topgen 17397  df-pt 17398  df-top 22877  df-topon 22894  df-bases 22929

This theorem is referenced by:  poimirlem30  38017