Theorem ptrest 38798

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 17644	. . . 4 ⊢ (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆)) = ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)
2		snex 5402	. . . . . . . 8 ⊢ {∪ (∏t‘𝐹)} ∈ V
3		ptrest.0	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		fvex 6927	. . . . . . . . . . 11 ⊢ (𝐹‘𝑢) ∈ V
5	4	rgenw 3084	. . . . . . . . . 10 ⊢ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V
6		eqid 2763	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))
7	6	mpoexxg 8121	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V) → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
8	3, 5, 7	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
9		rnexg 7946	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
10	8, 9	syl 18	. . . . . . . 8 ⊢ (𝜑 → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V)
11		unexg 7790	. . . . . . . 8 ⊢ (({∪ (∏t‘𝐹)} ∈ V ∧ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V)
12	2, 10, 11	sylancr 599	. . . . . . 7 ⊢ (𝜑 → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V)
13		ptrest.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊)
14	13	ralrimiva 3158	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊)
15		ixpexg 8986	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
16	14, 15	syl 18	. . . . . . 7 ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ V)
17		restval 17638	. . . . . . 7 ⊢ ((({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V ∧ X𝑘 ∈ 𝐴 𝑆 ∈ V) → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
18	12, 16, 17	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
19		mptun 6713	. . . . . . . . 9 ⊢ (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
20	19	rneqi 5929	. . . . . . . 8 ⊢ ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
21		rnun 6152	. . . . . . . 8 ⊢ ran ((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
22	20, 21	eqtri 2786	. . . . . . 7 ⊢ ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)))
23		elsni 4601	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → 𝑥 = ∪ (∏t‘𝐹))
24	23	ineq1d 4119	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
25	24	mpteq2ia 5204	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
26		fvex 6927	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) ∈ V
27	26	uniex 7788	. . . . . . . . . . . . 13 ⊢ ∪ (∏t‘𝐹) ∈ V
28	27	inex1 5282	. . . . . . . . . . . . 13 ⊢ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V
29		fmptsn 7201	. . . . . . . . . . . . 13 ⊢ ((∪ (∏t‘𝐹) ∈ V ∧ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V) → {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)))
30	27, 28, 29	mp2an 705	. . . . . . . . . . . 12 ⊢ {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
31	25, 30	eqtr4i 2789	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
32	31	rneqi 5929	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩}
33	27	rnsnop 6242	. . . . . . . . . 10 ⊢ ran {⟨∪ (∏t‘𝐹), (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)⟩} = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
34	32, 33	eqtri 2786	. . . . . . . . 9 ⊢ ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)}
35		ptrest.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝐴⟶Top)
36	35	ffvelcdmda 7114	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Top)
37		inss1 4136	. . . . . . . . . . . . . . 15 ⊢ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)
38		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
39	38	restuni 23524	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑘) ∈ Top ∧ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪ (𝐹‘𝑘)) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
40	36, 37, 39	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
41		fvex 6927	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑘) ∈ V
42	38	restin 23528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑘) ∈ V ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
43	41, 13, 42	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))))
44		incom 4109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ ∪ (𝐹‘𝑘)) = (∪ (𝐹‘𝑘) ∩ 𝑆)
45	44	oveq2i 7460	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))
46	43, 45	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
47	46	unieqd 4883	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)))
48	40, 47	eqtr4d 2801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t 𝑆))
49	48	ixpeq2dva 8976	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆))
50		ixpin 8987	. . . . . . . . . . . 12 ⊢ X𝑘 ∈ 𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆)
51		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∪ ((𝐹‘𝑘) ↾t 𝑆)
52		nfcv 2926	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(𝐹‘𝑦)
53		nfcv 2926	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘 ↾t
54		nfcsb1v 3875	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝑆
55	52, 53, 54	nfov 7479	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
56	55	nfuni 4877	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
57		fveq2 6914	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦))
58		csbeq1a 3865	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑦 → 𝑆 = ⦋𝑦 / 𝑘⦌𝑆)
59	57, 58	oveq12d 7467	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑦 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
60	59	unieqd 4883	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑦 → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
61	51, 56, 60	cbvixp 8978	. . . . . . . . . . . . 13 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
62		ixpeq2 8975	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
63		ovex 7482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V
64		nfcv 2926	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘𝑦
65		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))
66	64, 55, 59, 65	fvmptf 7044	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
67	63, 66	mpan2 704	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
68	67	unieqd 4883	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆))
69	62, 68	mprg 3086	. . . . . . . . . . . . 13 ⊢ X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)
70	61, 69	eqtr4i 2789	. . . . . . . . . . . 12 ⊢ X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦)
71	49, 50, 70	3eqtr3g 2821	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦))
72		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (∏t‘𝐹) = (∏t‘𝐹)
73	72	ptuni 23957	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
74	3, 35, 73	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ (∏t‘𝐹))
75	74	ineq1d 4119	. . . . . . . . . . 11 ⊢ (𝜑 → (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))
76		resttop 23522	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑘) ∈ Top ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
77	36, 13, 76	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top)
78	77	fmpttd 7145	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top)
79		eqid 2763	. . . . . . . . . . . . 13 ⊢ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
80	79	ptuni 23957	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
81	3, 78, 80	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
82	71, 75, 81	3eqtr3d 2806	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
83	82	sneqd 4596	. . . . . . . . 9 ⊢ (𝜑 → {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)} = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
84	34, 83	eqtrid 2810	. . . . . . . 8 ⊢ (𝜑 → ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))})
85		vex 3458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑤 ∈ V
86	85	elixp 8968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆))
87	86	simprbi 503	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆)
88		nfcsb1v 3875	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆
89	88	nfel2 2944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆
90		fveq2 6914	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → (𝑤‘𝑘) = (𝑤‘𝑢))
91		csbeq1a 3865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑢 → 𝑆 = ⦋𝑢 / 𝑘⦌𝑆)
92	90, 91	eleq12d 2858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑢 → ((𝑤‘𝑘) ∈ 𝑆 ↔ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
93	89, 92	rspc 3568	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
94	87, 93	syl5 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
95	94	pm4.71d 571	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
96	95	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))))
97		an4 669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
98		elin 4096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) ↔ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))
99	98	anbi2i 635	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))
100	97, 99	bitr4i 281	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
101	96, 100	bitrdi 290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
102		elin 4096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆))
103	82	eleq2d 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
104	102, 103	bitr3id 288	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))))
105	104	anbi1d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
106	101, 105	sylan9bbr 520	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
107	106	abbidv 2829	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))})
108		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢))
109	108	mptpreima 6256	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) = {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣}
110		df-rab 3417	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)}
111	109, 110	eqtr2i 2787	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)
112		abid2 2901	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆} = X𝑘 ∈ 𝐴 𝑆
113	111, 112	ineq12i 4118	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
114		inab 4257	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑤 ∣ (𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
115	113, 114	eqtr3i 2788	. . . . . . . . . . . . . . . 16 ⊢ ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = {𝑤 ∣ ((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)}
116		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢))
117	116	mptpreima 6256	. . . . . . . . . . . . . . . . 17 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)}
118		df-rab 3417	. . . . . . . . . . . . . . . . 17 ⊢ {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
119	117, 118	eqtri 2786	. . . . . . . . . . . . . . . 16 ⊢ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∣ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}
120	107, 115, 119	3eqtr4g 2823	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
121	120	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
122	121	rexbidv 3190	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
123		ineq1 4113	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑦 → (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))
124	123	imaeq2d 6068	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
125	124	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
126	125	cbvrexvw 3245	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
127	122, 126	bitrdi 290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
128		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
129	128	inex1 5282	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑦 ∈ (𝐹‘𝑢)) → (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V)
131		ovex 7482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V
132		nfcv 2926	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘𝑢
133		nfcv 2926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘(𝐹‘𝑢)
134	133, 53, 88	nfov 7479	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)
135		fveq2 6914	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (𝐹‘𝑘) = (𝐹‘𝑢))
136	135, 91	oveq12d 7467	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
137	132, 134, 136, 65	fvmptf 7044	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝐴 ∧ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
138	131, 137	mpan2 704	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
139	138	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))
140	139	eleq2d 2850	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)))
141		nfv 1949	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑢 ∈ 𝐴)
142		nfcsb1v 3875	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑊
143	88, 142	nfel 2940	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊
144	141, 143	nfim 1931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
145		eleq1w 2847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → (𝑘 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴))
146	145	anbi2d 642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴)))
147		csbeq1a 3865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → 𝑊 = ⦋𝑢 / 𝑘⦌𝑊)
148	91, 147	eleq12d 2858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (𝑆 ∈ 𝑊 ↔ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊))
149	146, 148	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)))
150	144, 149, 13	chvarfv 2280	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)
151		elrest 17639	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑢) ∈ V ∧ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
152	4, 150, 151	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
153	140, 152	bitrd 282	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
154		imaeq2 6064	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))
155	154	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
156	155	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)) → (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
157	130, 153, 156	rexxfr2d 5378	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))))
158	127, 157	bitr4d 285	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
159	158	rexbidva 3188	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
160	159	abbidv 2829	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)})
161		eqid 2763	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))
162	161	rnmpt 5949	. . . . . . . . . 10 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)}
163		nfre1 3291	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)
164		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)
165	27	mptex 7258	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
166	165	cnvex 7969	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V
167	166	imaex 7958	. . . . . . . . . . . . . 14 ⊢ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
168	167	rgen2w 3085	. . . . . . . . . . . . 13 ⊢ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V
169		ineq1 4113	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))
170	169	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
171	6, 170	rexrnmpo 7590	. . . . . . . . . . . . 13 ⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
172	168, 171	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))
173		eqeq1 2767	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
174	173	2rexbidv 3231	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
175	172, 174	bitrid 286	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)))
176	163, 164, 175	cbvabw 2835	. . . . . . . . . 10 ⊢ {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
177	162, 176	eqtri 2786	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)}
178		eqid 2763	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))
179	178	rnmpo 7583	. . . . . . . . 9 ⊢ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)}
180	160, 177, 179	3eqtr4g 2823	. . . . . . . 8 ⊢ (𝜑 → ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))
181	84, 180	uneq12d 4171	. . . . . . 7 ⊢ (𝜑 → (ran (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
182	22, 181	eqtrid 2810	. . . . . 6 ⊢ (𝜑 → ran (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
183	18, 182	eqtrd 2798	. . . . 5 ⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆) = ({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))
184	183	fveq2d 6918	. . . 4 ⊢ (𝜑 → (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈ 𝐴 𝑆)) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
185	1, 184	eqtr3id 2812	. . 3 ⊢ (𝜑 → ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))
186	185	fveq2d 6918	. 2 ⊢ (𝜑 → (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
187		eqid 2763	. . . . . 6 ⊢ ∪ (∏t‘𝐹) = ∪ (∏t‘𝐹)
188	72, 187, 6	ptval2 23964	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
189	3, 35, 188	syl2anc 596	. . . 4 ⊢ (𝜑 → (∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))))
190	189	oveq1d 7464	. . 3 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈ 𝐴 𝑆))
191		fvex 6927	. . . 4 ⊢ (fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ∈ V
192		tgrest 23521	. . . 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 599	. . 3 ⊢ (𝜑 → (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈ 𝐴 𝑆))
194	190, 193	eqtr4d 2801	. 2 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈ 𝐴 𝑆)))
195		eqid 2763	. . . 4 ⊢ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))
196	79, 195, 178	ptval2 23964	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
197	3, 78, 196	syl2anc 596	. 2 ⊢ (𝜑 → (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))))
198	186, 194, 197	3eqtr4d 2808	1 ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {cab 2741  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454  ⦋csb 3851   ⊆ wss 3900   ∩ cin 4092   ∪ cun 4152  {csn 4588  ⟨cop 4838  ∪ cuni 4870   ↦ cmpt 5190  ^◡ccnv 5655  ran crn 5657   “ cima 5659   Fn wfn 6559  ⟶wf 6560  ‘cfv 6564  (class class class)co 7449   ∈ cmpo 7451  Xcixp 8961  ficfi 9437   ↾_t crest 17632  topGenctg 17649  ∏_tcpt 17650  Topctop 23255

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-ov 7452  df-oprab 7453  df-mpo 7454  df-om 7910  df-1st 8033  df-2nd 8034  df-1o 8512  df-2o 8513  df-ixp 8962  df-en 9010  df-dom 9011  df-fin 9013  df-fi 9438  df-rest 17634  df-topgen 17655  df-pt 17656  df-top 23256  df-topon 23273  df-bases 23308

This theorem is used by:  poimirlem30  38829