ptrest

Description: Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019)

	Ref	Expression
Hypotheses	ptrest.0	$⊢ φ \to A \in V$
	ptrest.1	$⊢ φ \to F : A ⟶ Top$
	ptrest.2	$⊢ (φ \land k \in A) \to S \in W$
Assertion	ptrest	$⊢ φ \to \prod_{𝑡} (F) ↾_{𝑡} \underset{k \in A}{⨉} S = \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))$

Proof

Step	Hyp	Ref	Expression
1		ptrest.0	$⊢ φ \to A \in V$
2		ptrest.1	$⊢ φ \to F : A ⟶ Top$
3		ptrest.2	$⊢ (φ \land k \in A) \to S \in W$
4		firest	$⊢ fi ((\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S) = fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S$
5		snex	$⊢ \{⋃ \prod_{𝑡} (F)\} \in V$
6		fvex	$⊢ F (u) \in V$
7	6	rgenw	$⊢ \forall u \in A F (u) \in V$
8		eqid	$⊢ (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) = (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])$
9	8	mpoexxg	$⊢ (A \in V \land \forall u \in A F (u) \in V) \to (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V$
10	1 7 9	sylancl	$⊢ φ \to (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V$
11		rnexg	$⊢ (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V \to ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V$
12	10 11	syl	$⊢ φ \to ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V$
13		unexg	$⊢ (\{⋃ \prod_{𝑡} (F)\} \in V \land ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V) \to \{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V$
14	5 12 13	sylancr	$⊢ φ \to \{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V$
15	3	ralrimiva	$⊢ φ \to \forall k \in A S \in W$
16		ixpexg	$⊢ \forall k \in A S \in W \to \underset{k \in A}{⨉} S \in V$
17	15 16	syl	$⊢ φ \to \underset{k \in A}{⨉} S \in V$
18		restval	$⊢ (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) \in V \land \underset{k \in A}{⨉} S \in V) \to (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S = ran (x \in (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ⟼ x \cap \underset{k \in A}{⨉} S)$
19	14 17 18	syl2anc	$⊢ φ \to (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S = ran (x \in (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ⟼ x \cap \underset{k \in A}{⨉} S)$
20		mptun	$⊢ (x \in (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ⟼ x \cap \underset{k \in A}{⨉} S) = (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) \cup (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S)$
21	20	rneqi	$⊢ ran (x \in (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ⟼ x \cap \underset{k \in A}{⨉} S) = ran ((x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) \cup (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S))$
22		rnun	$⊢ ran ((x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) \cup (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S)) = ran (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) \cup ran (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S)$
23	21 22	eqtri	$⊢ ran (x \in (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ⟼ x \cap \underset{k \in A}{⨉} S) = ran (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) \cup ran (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S)$
24		elsni	$⊢ x \in \{⋃ \prod_{𝑡} (F)\} \to x = ⋃ \prod_{𝑡} (F)$
25	24	ineq1d	$⊢ x \in \{⋃ \prod_{𝑡} (F)\} \to x \cap \underset{k \in A}{⨉} S = ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S$
26	25	mpteq2ia	$⊢ (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) = (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S)$
27		fvex	$⊢ \prod_{𝑡} (F) \in V$
28	27	uniex	$⊢ ⋃ \prod_{𝑡} (F) \in V$
29	28	inex1	$⊢ ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S \in V$
30		fmptsn	$⊢ (⋃ \prod_{𝑡} (F) \in V \land ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S \in V) \to \{⟨⋃ \prod_{𝑡} (F), ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S⟩\} = (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S)$
31	28 29 30	mp2an	$⊢ \{⟨⋃ \prod_{𝑡} (F), ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S⟩\} = (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S)$
32	26 31	eqtr4i	$⊢ (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) = \{⟨⋃ \prod_{𝑡} (F), ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S⟩\}$
33	32	rneqi	$⊢ ran (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) = ran \{⟨⋃ \prod_{𝑡} (F), ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S⟩\}$
34	28	rnsnop	$⊢ ran \{⟨⋃ \prod_{𝑡} (F), ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S⟩\} = \{⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S\}$
35	33 34	eqtri	$⊢ ran (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) = \{⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S\}$
36	2	ffvelcdmda	$⊢ (φ \land k \in A) \to F (k) \in Top$
37		inss1	$⊢ ⋃ F (k) \cap S \subseteq ⋃ F (k)$
38		eqid	$⊢ ⋃ F (k) = ⋃ F (k)$
39	38	restuni	$⊢ (F (k) \in Top \land ⋃ F (k) \cap S \subseteq ⋃ F (k)) \to ⋃ F (k) \cap S = ⋃ (F (k) ↾_{𝑡} (⋃ F (k) \cap S))$
40	36 37 39	sylancl	$⊢ (φ \land k \in A) \to ⋃ F (k) \cap S = ⋃ (F (k) ↾_{𝑡} (⋃ F (k) \cap S))$
41		fvex	$⊢ F (k) \in V$
42	38	restin	$⊢ (F (k) \in V \land S \in W) \to F (k) ↾_{𝑡} S = F (k) ↾_{𝑡} (S \cap ⋃ F (k))$
43	41 3 42	sylancr	$⊢ (φ \land k \in A) \to F (k) ↾_{𝑡} S = F (k) ↾_{𝑡} (S \cap ⋃ F (k))$
44		incom	$⊢ S \cap ⋃ F (k) = ⋃ F (k) \cap S$
45	44	oveq2i	$⊢ F (k) ↾_{𝑡} (S \cap ⋃ F (k)) = F (k) ↾_{𝑡} (⋃ F (k) \cap S)$
46	43 45	eqtrdi	$⊢ (φ \land k \in A) \to F (k) ↾_{𝑡} S = F (k) ↾_{𝑡} (⋃ F (k) \cap S)$
47	46	unieqd	$⊢ (φ \land k \in A) \to ⋃ (F (k) ↾_{𝑡} S) = ⋃ (F (k) ↾_{𝑡} (⋃ F (k) \cap S))$
48	40 47	eqtr4d	$⊢ (φ \land k \in A) \to ⋃ F (k) \cap S = ⋃ (F (k) ↾_{𝑡} S)$
49	48	ixpeq2dva	$⊢ φ \to \underset{k \in A}{⨉} (⋃ F (k) \cap S) = \underset{k \in A}{⨉} ⋃ (F (k) ↾_{𝑡} S)$
50		ixpin	$⊢ \underset{k \in A}{⨉} (⋃ F (k) \cap S) = \underset{k \in A}{⨉} ⋃ F (k) \cap \underset{k \in A}{⨉} S$
51		nfcv	$⊢ \underline{Ⅎ} y ⋃ (F (k) ↾_{𝑡} S)$
52		nfcv	$⊢ \underline{Ⅎ} k F (y)$
53		nfcv	$⊢ \underline{Ⅎ} k ↾_{𝑡}$
54		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ S$
55	52 53 54	nfov	$⊢ \underline{Ⅎ} k (F (y) ↾_{𝑡} ⦋ y / k ⦌ S)$
56	55	nfuni	$⊢ \underline{Ⅎ} k ⋃ (F (y) ↾_{𝑡} ⦋ y / k ⦌ S)$
57		fveq2	$⊢ k = y \to F (k) = F (y)$
58		csbeq1a	$⊢ k = y \to S = ⦋ y / k ⦌ S$
59	57 58	oveq12d	$⊢ k = y \to F (k) ↾_{𝑡} S = F (y) ↾_{𝑡} ⦋ y / k ⦌ S$
60	59	unieqd	$⊢ k = y \to ⋃ (F (k) ↾_{𝑡} S) = ⋃ (F (y) ↾_{𝑡} ⦋ y / k ⦌ S)$
61	51 56 60	cbvixp	$⊢ \underset{k \in A}{⨉} ⋃ (F (k) ↾_{𝑡} S) = \underset{y \in A}{⨉} ⋃ (F (y) ↾_{𝑡} ⦋ y / k ⦌ S)$
62		ixpeq2	$⊢ \forall y \in A ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = ⋃ (F (y) ↾_{𝑡} ⦋ y / k ⦌ S) \to \underset{y \in A}{⨉} ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = \underset{y \in A}{⨉} ⋃ (F (y) ↾_{𝑡} ⦋ y / k ⦌ S)$
63		ovex	$⊢ F (y) ↾_{𝑡} ⦋ y / k ⦌ S \in V$
64		nfcv	$⊢ \underline{Ⅎ} k y$
65		eqid	$⊢ (k \in A ⟼ F (k) ↾_{𝑡} S) = (k \in A ⟼ F (k) ↾_{𝑡} S)$
66	64 55 59 65	fvmptf	$⊢ (y \in A \land F (y) ↾_{𝑡} ⦋ y / k ⦌ S \in V) \to (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = F (y) ↾_{𝑡} ⦋ y / k ⦌ S$
67	63 66	mpan2	$⊢ y \in A \to (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = F (y) ↾_{𝑡} ⦋ y / k ⦌ S$
68	67	unieqd	$⊢ y \in A \to ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = ⋃ (F (y) ↾_{𝑡} ⦋ y / k ⦌ S)$
69	62 68	mprg	$⊢ \underset{y \in A}{⨉} ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = \underset{y \in A}{⨉} ⋃ (F (y) ↾_{𝑡} ⦋ y / k ⦌ S)$
70	61 69	eqtr4i	$⊢ \underset{k \in A}{⨉} ⋃ (F (k) ↾_{𝑡} S) = \underset{y \in A}{⨉} ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y)$
71	49 50 70	3eqtr3g	$⊢ φ \to \underset{k \in A}{⨉} ⋃ F (k) \cap \underset{k \in A}{⨉} S = \underset{y \in A}{⨉} ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y)$
72		eqid	$⊢ \prod_{𝑡} (F) = \prod_{𝑡} (F)$
73	72	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ \prod_{𝑡} (F)$
74	1 2 73	syl2anc	$⊢ φ \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ \prod_{𝑡} (F)$
75	74	ineq1d	$⊢ φ \to \underset{k \in A}{⨉} ⋃ F (k) \cap \underset{k \in A}{⨉} S = ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S$
76		resttop	$⊢ (F (k) \in Top \land S \in W) \to F (k) ↾_{𝑡} S \in Top$
77	36 3 76	syl2anc	$⊢ (φ \land k \in A) \to F (k) ↾_{𝑡} S \in Top$
78	77	fmpttd	$⊢ φ \to (k \in A ⟼ F (k) ↾_{𝑡} S) : A ⟶ Top$
79		eqid	$⊢ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) = \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))$
80	79	ptuni	$⊢ (A \in V \land (k \in A ⟼ F (k) ↾_{𝑡} S) : A ⟶ Top) \to \underset{y \in A}{⨉} ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))$
81	1 78 80	syl2anc	$⊢ φ \to \underset{y \in A}{⨉} ⋃ (k \in A ⟼ F (k) ↾_{𝑡} S) (y) = ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))$
82	71 75 81	3eqtr3d	$⊢ φ \to ⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S = ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))$
83	82	sneqd	$⊢ φ \to \{⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S\} = \{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\}$
84	35 83	eqtrid	$⊢ φ \to ran (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) = \{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\}$
85		vex	$⊢ w \in V$
86	85	elixp	$⊢ w \in \underset{k \in A}{⨉} S \leftrightarrow (w Fn A \land \forall k \in A w (k) \in S)$
87	86	simprbi	$⊢ w \in \underset{k \in A}{⨉} S \to \forall k \in A w (k) \in S$
88		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ u / k ⦌ S$
89	88	nfel2	$⊢ Ⅎ k w (u) \in ⦋ u / k ⦌ S$
90		fveq2	$⊢ k = u \to w (k) = w (u)$
91		csbeq1a	$⊢ k = u \to S = ⦋ u / k ⦌ S$
92	90 91	eleq12d	$⊢ k = u \to (w (k) \in S \leftrightarrow w (u) \in ⦋ u / k ⦌ S)$
93	89 92	rspc	$⊢ u \in A \to (\forall k \in A w (k) \in S \to w (u) \in ⦋ u / k ⦌ S)$
94	87 93	syl5	$⊢ u \in A \to (w \in \underset{k \in A}{⨉} S \to w (u) \in ⦋ u / k ⦌ S)$
95	94	pm4.71d	$⊢ u \in A \to (w \in \underset{k \in A}{⨉} S \leftrightarrow (w \in \underset{k \in A}{⨉} S \land w (u) \in ⦋ u / k ⦌ S))$
96	95	anbi2d	$⊢ u \in A \to (((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land w \in \underset{k \in A}{⨉} S) \leftrightarrow ((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land (w \in \underset{k \in A}{⨉} S \land w (u) \in ⦋ u / k ⦌ S)))$
97		an4	$⊢ ((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land (w \in \underset{k \in A}{⨉} S \land w (u) \in ⦋ u / k ⦌ S)) \leftrightarrow ((w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S) \land (w (u) \in v \land w (u) \in ⦋ u / k ⦌ S))$
98		elin	$⊢ w (u) \in (v \cap ⦋ u / k ⦌ S) \leftrightarrow (w (u) \in v \land w (u) \in ⦋ u / k ⦌ S)$
99	98	anbi2i	$⊢ ((w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S) \land w (u) \in (v \cap ⦋ u / k ⦌ S)) \leftrightarrow ((w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S) \land (w (u) \in v \land w (u) \in ⦋ u / k ⦌ S))$
100	97 99	bitr4i	$⊢ ((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land (w \in \underset{k \in A}{⨉} S \land w (u) \in ⦋ u / k ⦌ S)) \leftrightarrow ((w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S) \land w (u) \in (v \cap ⦋ u / k ⦌ S))$
101	96 100	bitrdi	$⊢ u \in A \to (((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land w \in \underset{k \in A}{⨉} S) \leftrightarrow ((w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S) \land w (u) \in (v \cap ⦋ u / k ⦌ S)))$
102		elin	$⊢ w \in (⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S) \leftrightarrow (w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S)$
103	82	eleq2d	$⊢ φ \to (w \in (⋃ \prod_{𝑡} (F) \cap \underset{k \in A}{⨉} S) \leftrightarrow w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)))$
104	102 103	bitr3id	$⊢ φ \to ((w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S) \leftrightarrow w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)))$
105	104	anbi1d	$⊢ φ \to (((w \in ⋃ \prod_{𝑡} (F) \land w \in \underset{k \in A}{⨉} S) \land w (u) \in (v \cap ⦋ u / k ⦌ S)) \leftrightarrow (w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) \land w (u) \in (v \cap ⦋ u / k ⦌ S)))$
106	101 105	sylan9bbr	$⊢ (φ \land u \in A) \to (((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land w \in \underset{k \in A}{⨉} S) \leftrightarrow (w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) \land w (u) \in (v \cap ⦋ u / k ⦌ S)))$
107	106	abbidv	$⊢ (φ \land u \in A) \to \{w \| ((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land w \in \underset{k \in A}{⨉} S)\} = \{w \| (w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) \land w (u) \in (v \cap ⦋ u / k ⦌ S))\}$
108		eqid	$⊢ (w \in ⋃ \prod_{𝑡} (F) ⟼ w (u)) = (w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))$
109	108	mptpreima	$⊢ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] = \{w \in ⋃ \prod_{𝑡} (F) \| w (u) \in v\}$
110		df-rab	$⊢ \{w \in ⋃ \prod_{𝑡} (F) \| w (u) \in v\} = \{w \| (w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v)\}$
111	109 110	eqtr2i	$⊢ \{w \| (w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v)\} = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]$
112		abid2	$⊢ \{w \| w \in \underset{k \in A}{⨉} S\} = \underset{k \in A}{⨉} S$
113	111 112	ineq12i	$⊢ \{w \| (w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v)\} \cap \{w \| w \in \underset{k \in A}{⨉} S\} = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S$
114		inab	$⊢ \{w \| (w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v)\} \cap \{w \| w \in \underset{k \in A}{⨉} S\} = \{w \| ((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land w \in \underset{k \in A}{⨉} S)\}$
115	113 114	eqtr3i	$⊢ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S = \{w \| ((w \in ⋃ \prod_{𝑡} (F) \land w (u) \in v) \land w \in \underset{k \in A}{⨉} S)\}$
116		eqid	$⊢ (w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u)) = (w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))$
117	116	mptpreima	$⊢ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S] = \{w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) \| w (u) \in (v \cap ⦋ u / k ⦌ S)\}$
118		df-rab	$⊢ \{w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) \| w (u) \in (v \cap ⦋ u / k ⦌ S)\} = \{w \| (w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) \land w (u) \in (v \cap ⦋ u / k ⦌ S))\}$
119	117 118	eqtri	$⊢ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S] = \{w \| (w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) \land w (u) \in (v \cap ⦋ u / k ⦌ S))\}$
120	107 115 119	3eqtr4g	$⊢ (φ \land u \in A) \to {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S]$
121	120	eqeq2d	$⊢ (φ \land u \in A) \to (x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S \leftrightarrow x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S])$
122	121	rexbidv	$⊢ (φ \land u \in A) \to (\exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S \leftrightarrow \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S])$
123		ineq1	$⊢ v = y \to v \cap ⦋ u / k ⦌ S = y \cap ⦋ u / k ⦌ S$
124	123	imaeq2d	$⊢ v = y \to {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S] = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S]$
125	124	eqeq2d	$⊢ v = y \to (x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S] \leftrightarrow x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S])$
126	125	cbvrexvw	$⊢ \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v \cap ⦋ u / k ⦌ S] \leftrightarrow \exists y \in F (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S]$
127	122 126	bitrdi	$⊢ (φ \land u \in A) \to (\exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S \leftrightarrow \exists y \in F (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S])$
128		vex	$⊢ y \in V$
129	128	inex1	$⊢ y \cap ⦋ u / k ⦌ S \in V$
130	129	a1i	$⊢ ((φ \land u \in A) \land y \in F (u)) \to y \cap ⦋ u / k ⦌ S \in V$
131		ovex	$⊢ F (u) ↾_{𝑡} ⦋ u / k ⦌ S \in V$
132		nfcv	$⊢ \underline{Ⅎ} k u$
133		nfcv	$⊢ \underline{Ⅎ} k F (u)$
134	133 53 88	nfov	$⊢ \underline{Ⅎ} k (F (u) ↾_{𝑡} ⦋ u / k ⦌ S)$
135		fveq2	$⊢ k = u \to F (k) = F (u)$
136	135 91	oveq12d	$⊢ k = u \to F (k) ↾_{𝑡} S = F (u) ↾_{𝑡} ⦋ u / k ⦌ S$
137	132 134 136 65	fvmptf	$⊢ (u \in A \land F (u) ↾_{𝑡} ⦋ u / k ⦌ S \in V) \to (k \in A ⟼ F (k) ↾_{𝑡} S) (u) = F (u) ↾_{𝑡} ⦋ u / k ⦌ S$
138	131 137	mpan2	$⊢ u \in A \to (k \in A ⟼ F (k) ↾_{𝑡} S) (u) = F (u) ↾_{𝑡} ⦋ u / k ⦌ S$
139	138	adantl	$⊢ (φ \land u \in A) \to (k \in A ⟼ F (k) ↾_{𝑡} S) (u) = F (u) ↾_{𝑡} ⦋ u / k ⦌ S$
140	139	eleq2d	$⊢ (φ \land u \in A) \to (v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) \leftrightarrow v \in (F (u) ↾_{𝑡} ⦋ u / k ⦌ S))$
141		nfv	$⊢ Ⅎ k (φ \land u \in A)$
142		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ u / k ⦌ W$
143	88 142	nfel	$⊢ Ⅎ k ⦋ u / k ⦌ S \in ⦋ u / k ⦌ W$
144	141 143	nfim	$⊢ Ⅎ k ((φ \land u \in A) \to ⦋ u / k ⦌ S \in ⦋ u / k ⦌ W)$
145		eleq1w	$⊢ k = u \to (k \in A \leftrightarrow u \in A)$
146	145	anbi2d	$⊢ k = u \to ((φ \land k \in A) \leftrightarrow (φ \land u \in A))$
147		csbeq1a	$⊢ k = u \to W = ⦋ u / k ⦌ W$
148	91 147	eleq12d	$⊢ k = u \to (S \in W \leftrightarrow ⦋ u / k ⦌ S \in ⦋ u / k ⦌ W)$
149	146 148	imbi12d	$⊢ k = u \to (((φ \land k \in A) \to S \in W) \leftrightarrow ((φ \land u \in A) \to ⦋ u / k ⦌ S \in ⦋ u / k ⦌ W))$
150	144 149 3	chvarfv	$⊢ (φ \land u \in A) \to ⦋ u / k ⦌ S \in ⦋ u / k ⦌ W$
151		elrest	$⊢ (F (u) \in V \land ⦋ u / k ⦌ S \in ⦋ u / k ⦌ W) \to (v \in (F (u) ↾_{𝑡} ⦋ u / k ⦌ S) \leftrightarrow \exists y \in F (u) v = y \cap ⦋ u / k ⦌ S)$
152	6 150 151	sylancr	$⊢ (φ \land u \in A) \to (v \in (F (u) ↾_{𝑡} ⦋ u / k ⦌ S) \leftrightarrow \exists y \in F (u) v = y \cap ⦋ u / k ⦌ S)$
153	140 152	bitrd	$⊢ (φ \land u \in A) \to (v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) \leftrightarrow \exists y \in F (u) v = y \cap ⦋ u / k ⦌ S)$
154		imaeq2	$⊢ v = y \cap ⦋ u / k ⦌ S \to {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v] = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S]$
155	154	eqeq2d	$⊢ v = y \cap ⦋ u / k ⦌ S \to (x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v] \leftrightarrow x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S])$
156	155	adantl	$⊢ ((φ \land u \in A) \land v = y \cap ⦋ u / k ⦌ S) \to (x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v] \leftrightarrow x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S])$
157	130 153 156	rexxfr2d	$⊢ (φ \land u \in A) \to (\exists v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v] \leftrightarrow \exists y \in F (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [y \cap ⦋ u / k ⦌ S])$
158	127 157	bitr4d	$⊢ (φ \land u \in A) \to (\exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S \leftrightarrow \exists v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])$
159	158	rexbidva	$⊢ φ \to (\exists u \in A \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S \leftrightarrow \exists u \in A \exists v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])$
160	159	abbidv	$⊢ φ \to \{x \| \exists u \in A \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S\} = \{x \| \exists u \in A \exists v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v]\}$
161		eqid	$⊢ (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S) = (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S)$
162	161	rnmpt	$⊢ ran (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S) = \{y \| \exists x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) y = x \cap \underset{k \in A}{⨉} S\}$
163		nfre1	$⊢ Ⅎ x \exists x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) y = x \cap \underset{k \in A}{⨉} S$
164		nfv	$⊢ Ⅎ y \exists u \in A \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S$
165	28	mptex	$⊢ (w \in ⋃ \prod_{𝑡} (F) ⟼ w (u)) \in V$
166	165	cnvex	$⊢ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} \in V$
167	166	imaex	$⊢ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \in V$
168	167	rgen2w	$⊢ \forall u \in A \forall v \in F (u) {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \in V$
169		ineq1	$⊢ x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \to x \cap \underset{k \in A}{⨉} S = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S$
170	169	eqeq2d	$⊢ x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \to (y = x \cap \underset{k \in A}{⨉} S \leftrightarrow y = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S)$
171	8 170	rexrnmpo	$⊢ \forall u \in A \forall v \in F (u) {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \in V \to (\exists x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) y = x \cap \underset{k \in A}{⨉} S \leftrightarrow \exists u \in A \exists v \in F (u) y = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S)$
172	168 171	ax-mp	$⊢ \exists x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) y = x \cap \underset{k \in A}{⨉} S \leftrightarrow \exists u \in A \exists v \in F (u) y = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S$
173		eqeq1	$⊢ y = x \to (y = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S \leftrightarrow x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S)$
174	173	2rexbidv	$⊢ y = x \to (\exists u \in A \exists v \in F (u) y = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S \leftrightarrow \exists u \in A \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S)$
175	172 174	bitrid	$⊢ y = x \to (\exists x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) y = x \cap \underset{k \in A}{⨉} S \leftrightarrow \exists u \in A \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S)$
176	163 164 175	cbvabw	$⊢ \{y \| \exists x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) y = x \cap \underset{k \in A}{⨉} S\} = \{x \| \exists u \in A \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S\}$
177	162 176	eqtri	$⊢ ran (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S) = \{x \| \exists u \in A \exists v \in F (u) x = {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v] \cap \underset{k \in A}{⨉} S\}$
178		eqid	$⊢ (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v]) = (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])$
179	178	rnmpo	$⊢ ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v]) = \{x \| \exists u \in A \exists v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) x = {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v]\}$
180	160 177 179	3eqtr4g	$⊢ φ \to ran (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S) = ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])$
181	84 180	uneq12d	$⊢ φ \to ran (x \in \{⋃ \prod_{𝑡} (F)\} ⟼ x \cap \underset{k \in A}{⨉} S) \cup ran (x \in ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]) ⟼ x \cap \underset{k \in A}{⨉} S) = \{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])$
182	23 181	eqtrid	$⊢ φ \to ran (x \in (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ⟼ x \cap \underset{k \in A}{⨉} S) = \{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])$
183	19 182	eqtrd	$⊢ φ \to (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S = \{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])$
184	183	fveq2d	$⊢ φ \to fi ((\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S) = fi (\{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v]))$
185	4 184	eqtr3id	$⊢ φ \to fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S = fi (\{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v]))$
186	185	fveq2d	$⊢ φ \to topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S) = topGen (fi (\{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])))$
187		eqid	$⊢ ⋃ \prod_{𝑡} (F) = ⋃ \prod_{𝑡} (F)$
188	72 187 8	ptval2	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) = topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])))$
189	1 2 188	syl2anc	$⊢ φ \to \prod_{𝑡} (F) = topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])))$
190	189	oveq1d	$⊢ φ \to \prod_{𝑡} (F) ↾_{𝑡} \underset{k \in A}{⨉} S = topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]))) ↾_{𝑡} \underset{k \in A}{⨉} S$
191		fvex	$⊢ fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) \in V$
192		tgrest	$⊢ (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) \in V \land \underset{k \in A}{⨉} S \in V) \to topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S) = topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]))) ↾_{𝑡} \underset{k \in A}{⨉} S$
193	191 17 192	sylancr	$⊢ φ \to topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S) = topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v]))) ↾_{𝑡} \underset{k \in A}{⨉} S$
194	190 193	eqtr4d	$⊢ φ \to \prod_{𝑡} (F) ↾_{𝑡} \underset{k \in A}{⨉} S = topGen (fi (\{⋃ \prod_{𝑡} (F)\} \cup ran (u \in A, v \in F (u) ⟼ {(w \in ⋃ \prod_{𝑡} (F) ⟼ w (u))}^{-1} [v])) ↾_{𝑡} \underset{k \in A}{⨉} S)$
195		eqid	$⊢ ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) = ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))$
196	79 195 178	ptval2	$⊢ (A \in V \land (k \in A ⟼ F (k) ↾_{𝑡} S) : A ⟶ Top) \to \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) = topGen (fi (\{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])))$
197	1 78 196	syl2anc	$⊢ φ \to \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) = topGen (fi (\{⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))\} \cup ran (u \in A, v \in (k \in A ⟼ F (k) ↾_{𝑡} S) (u) ⟼ {(w \in ⋃ \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S)) ⟼ w (u))}^{-1} [v])))$
198	186 194 197	3eqtr4d	$⊢ φ \to \prod_{𝑡} (F) ↾_{𝑡} \underset{k \in A}{⨉} S = \prod_{𝑡} ((k \in A ⟼ F (k) ↾_{𝑡} S))$

Metamath Proof Explorer

Theorem ptrest

Proof