ptbasfi

Description: The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add X itself to the list because if A is empty we get ( fi(/) ) = (/) while B = { (/) } .) (Contributed by Mario Carneiro, 3-Feb-2015)

	Ref	Expression
Hypotheses	ptbas.1	$⊢ B = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
	ptbasfi.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
Assertion	ptbasfi	$⊢ (A \in V \land F : A ⟶ Top) \to B = fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$

Proof

Step	Hyp	Ref	Expression
1		ptbas.1	$⊢ B = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
2		ptbasfi.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
3	1	elpt	$⊢ s \in B \leftrightarrow \exists h ((h Fn A \land \forall y \in A h (y) \in F (y) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} h (y))$
4		df-3an	$⊢ (h Fn A \land \forall y \in A h (y) \in F (y) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y)) \leftrightarrow ((h Fn A \land \forall y \in A h (y) \in F (y)) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y))$
5		simprr	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \forall y \in (A ∖ m) h (y) = ⋃ F (y)$
6		disjdif2	$⊢ A \cap m = \emptyset \to A ∖ m = A$
7	6	raleqdv	$⊢ A \cap m = \emptyset \to (\forall y \in (A ∖ m) h (y) = ⋃ F (y) \leftrightarrow \forall y \in A h (y) = ⋃ F (y))$
8	7	biimpac	$⊢ (\forall y \in (A ∖ m) h (y) = ⋃ F (y) \land A \cap m = \emptyset) \to \forall y \in A h (y) = ⋃ F (y)$
9		ixpeq2	$⊢ \forall y \in A h (y) = ⋃ F (y) \to \underset{y \in A}{⨉} h (y) = \underset{y \in A}{⨉} ⋃ F (y)$
10	8 9	syl	$⊢ (\forall y \in (A ∖ m) h (y) = ⋃ F (y) \land A \cap m = \emptyset) \to \underset{y \in A}{⨉} h (y) = \underset{y \in A}{⨉} ⋃ F (y)$
11		fveq2	$⊢ n = y \to F (n) = F (y)$
12	11	unieqd	$⊢ n = y \to ⋃ F (n) = ⋃ F (y)$
13	12	cbvixpv	$⊢ \underset{n \in A}{⨉} ⋃ F (n) = \underset{y \in A}{⨉} ⋃ F (y)$
14	2 13	eqtri	$⊢ X = \underset{y \in A}{⨉} ⋃ F (y)$
15	10 14	eqtr4di	$⊢ (\forall y \in (A ∖ m) h (y) = ⋃ F (y) \land A \cap m = \emptyset) \to \underset{y \in A}{⨉} h (y) = X$
16	5 15	sylan	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m = \emptyset) \to \underset{y \in A}{⨉} h (y) = X$
17		ssv	$⊢ X \subseteq V$
18		iineq1	$⊢ A \cap m = \emptyset \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = ⋂_{n \in \emptyset} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
19		0iin	$⊢ ⋂_{n \in \emptyset} {(w \in X ⟼ w (n))}^{-1} [h (n)] = V$
20	18 19	eqtrdi	$⊢ A \cap m = \emptyset \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = V$
21	17 20	sseqtrrid	$⊢ A \cap m = \emptyset \to X \subseteq ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
22	21	adantl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m = \emptyset) \to X \subseteq ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
23		df-ss	$⊢ X \subseteq ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \leftrightarrow X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = X$
24	22 23	sylib	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m = \emptyset) \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = X$
25	16 24	eqtr4d	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m = \emptyset) \to \underset{y \in A}{⨉} h (y) = X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
26		simplll	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to (A \in V \land F : A ⟶ Top)$
27		inss1	$⊢ A \cap m \subseteq A$
28		simpr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to n \in (A \cap m)$
29	27 28	sseldi	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to n \in A$
30		fveq2	$⊢ y = n \to h (y) = h (n)$
31		fveq2	$⊢ y = n \to F (y) = F (n)$
32	30 31	eleq12d	$⊢ y = n \to (h (y) \in F (y) \leftrightarrow h (n) \in F (n))$
33		simprr	$⊢ ((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \to \forall y \in A h (y) \in F (y)$
34	33	ad2antrr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to \forall y \in A h (y) \in F (y)$
35	32 34 29	rspcdva	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to h (n) \in F (n)$
36	14	ptpjpre1	$⊢ ((A \in V \land F : A ⟶ Top) \land (n \in A \land h (n) \in F (n))) \to {(w \in X ⟼ w (n))}^{-1} [h (n)] = \underset{y \in A}{⨉} if (y = n, h (n), ⋃ F (y))$
37	26 29 35 36	syl12anc	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to {(w \in X ⟼ w (n))}^{-1} [h (n)] = \underset{y \in A}{⨉} if (y = n, h (n), ⋃ F (y))$
38	37	adantlr	$⊢ (((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \land n \in (A \cap m)) \to {(w \in X ⟼ w (n))}^{-1} [h (n)] = \underset{y \in A}{⨉} if (y = n, h (n), ⋃ F (y))$
39	38	iineq2dv	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = ⋂_{n \in A \cap m} \underset{y \in A}{⨉} if (y = n, h (n), ⋃ F (y))$
40		simpr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to A \cap m \neq \emptyset$
41		cnvimass	$⊢ {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq dom (w \in X ⟼ w (n))$
42		eqid	$⊢ (w \in X ⟼ w (n)) = (w \in X ⟼ w (n))$
43	42	dmmptss	$⊢ dom (w \in X ⟼ w (n)) \subseteq X$
44	41 43	sstri	$⊢ {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq X$
45	44 14	sseqtri	$⊢ {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
46	45	rgenw	$⊢ \forall n \in (A \cap m) {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
47		r19.2z	$⊢ (A \cap m \neq \emptyset \land \forall n \in (A \cap m) {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y)) \to \exists n \in (A \cap m) {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
48	40 46 47	sylancl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \exists n \in (A \cap m) {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
49		iinss	$⊢ \exists n \in (A \cap m) {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
50	48 49	syl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq \underset{y \in A}{⨉} ⋃ F (y)$
51	50 14	sseqtrrdi	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq X$
52		sseqin2	$⊢ ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq X \leftrightarrow X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
53	51 52	sylib	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
54	33	ad2antrr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \forall y \in A h (y) \in F (y)$
55		ssralv	$⊢ A \cap m \subseteq A \to (\forall y \in A h (y) \in F (y) \to \forall y \in (A \cap m) h (y) \in F (y))$
56	27 55	ax-mp	$⊢ \forall y \in A h (y) \in F (y) \to \forall y \in (A \cap m) h (y) \in F (y)$
57		elssuni	$⊢ h (y) \in F (y) \to h (y) \subseteq ⋃ F (y)$
58		iffalse	$⊢ \neg y = n \to if (y = n, h (n), ⋃ F (y)) = ⋃ F (y)$
59	58	sseq2d	$⊢ \neg y = n \to (h (y) \subseteq if (y = n, h (n), ⋃ F (y)) \leftrightarrow h (y) \subseteq ⋃ F (y))$
60	57 59	syl5ibrcom	$⊢ h (y) \in F (y) \to (\neg y = n \to h (y) \subseteq if (y = n, h (n), ⋃ F (y)))$
61		ssid	$⊢ h (y) \subseteq h (y)$
62		iftrue	$⊢ y = n \to if (y = n, h (n), ⋃ F (y)) = h (n)$
63	62 30	eqtr4d	$⊢ y = n \to if (y = n, h (n), ⋃ F (y)) = h (y)$
64	61 63	sseqtrrid	$⊢ y = n \to h (y) \subseteq if (y = n, h (n), ⋃ F (y))$
65	60 64	pm2.61d2	$⊢ h (y) \in F (y) \to h (y) \subseteq if (y = n, h (n), ⋃ F (y))$
66	65	ralrimivw	$⊢ h (y) \in F (y) \to \forall n \in (A \cap m) h (y) \subseteq if (y = n, h (n), ⋃ F (y))$
67		ssiin	$⊢ h (y) \subseteq ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \leftrightarrow \forall n \in (A \cap m) h (y) \subseteq if (y = n, h (n), ⋃ F (y))$
68	66 67	sylibr	$⊢ h (y) \in F (y) \to h (y) \subseteq ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
69	68	adantl	$⊢ (y \in (A \cap m) \land h (y) \in F (y)) \to h (y) \subseteq ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
70	62	equcoms	$⊢ n = y \to if (y = n, h (n), ⋃ F (y)) = h (n)$
71		fveq2	$⊢ n = y \to h (n) = h (y)$
72	70 71	eqtrd	$⊢ n = y \to if (y = n, h (n), ⋃ F (y)) = h (y)$
73	72	sseq1d	$⊢ n = y \to (if (y = n, h (n), ⋃ F (y)) \subseteq h (y) \leftrightarrow h (y) \subseteq h (y))$
74	73	rspcev	$⊢ (y \in (A \cap m) \land h (y) \subseteq h (y)) \to \exists n \in (A \cap m) if (y = n, h (n), ⋃ F (y)) \subseteq h (y)$
75	61 74	mpan2	$⊢ y \in (A \cap m) \to \exists n \in (A \cap m) if (y = n, h (n), ⋃ F (y)) \subseteq h (y)$
76		iinss	$⊢ \exists n \in (A \cap m) if (y = n, h (n), ⋃ F (y)) \subseteq h (y) \to ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \subseteq h (y)$
77	75 76	syl	$⊢ y \in (A \cap m) \to ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \subseteq h (y)$
78	77	adantr	$⊢ (y \in (A \cap m) \land h (y) \in F (y)) \to ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \subseteq h (y)$
79	69 78	eqssd	$⊢ (y \in (A \cap m) \land h (y) \in F (y)) \to h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
80	79	ralimiaa	$⊢ \forall y \in (A \cap m) h (y) \in F (y) \to \forall y \in (A \cap m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
81	54 56 80	3syl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \forall y \in (A \cap m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
82		eldifn	$⊢ y \in (A ∖ m) \to \neg y \in m$
83	82	ad2antlr	$⊢ ((A \cap m \neq \emptyset \land y \in (A ∖ m)) \land n \in (A \cap m)) \to \neg y \in m$
84		inss2	$⊢ A \cap m \subseteq m$
85		simpr	$⊢ ((A \cap m \neq \emptyset \land y \in (A ∖ m)) \land n \in (A \cap m)) \to n \in (A \cap m)$
86	84 85	sseldi	$⊢ ((A \cap m \neq \emptyset \land y \in (A ∖ m)) \land n \in (A \cap m)) \to n \in m$
87		eleq1	$⊢ y = n \to (y \in m \leftrightarrow n \in m)$
88	86 87	syl5ibrcom	$⊢ ((A \cap m \neq \emptyset \land y \in (A ∖ m)) \land n \in (A \cap m)) \to (y = n \to y \in m)$
89	83 88	mtod	$⊢ ((A \cap m \neq \emptyset \land y \in (A ∖ m)) \land n \in (A \cap m)) \to \neg y = n$
90	89 58	syl	$⊢ ((A \cap m \neq \emptyset \land y \in (A ∖ m)) \land n \in (A \cap m)) \to if (y = n, h (n), ⋃ F (y)) = ⋃ F (y)$
91	90	iineq2dv	$⊢ (A \cap m \neq \emptyset \land y \in (A ∖ m)) \to ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) = ⋂_{n \in A \cap m} ⋃ F (y)$
92		iinconst	$⊢ A \cap m \neq \emptyset \to ⋂_{n \in A \cap m} ⋃ F (y) = ⋃ F (y)$
93	92	adantr	$⊢ (A \cap m \neq \emptyset \land y \in (A ∖ m)) \to ⋂_{n \in A \cap m} ⋃ F (y) = ⋃ F (y)$
94	91 93	eqtr2d	$⊢ (A \cap m \neq \emptyset \land y \in (A ∖ m)) \to ⋃ F (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
95		eqeq1	$⊢ h (y) = ⋃ F (y) \to (h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \leftrightarrow ⋃ F (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)))$
96	94 95	syl5ibrcom	$⊢ (A \cap m \neq \emptyset \land y \in (A ∖ m)) \to (h (y) = ⋃ F (y) \to h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)))$
97	96	ralimdva	$⊢ A \cap m \neq \emptyset \to (\forall y \in (A ∖ m) h (y) = ⋃ F (y) \to \forall y \in (A ∖ m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)))$
98	5 97	mpan9	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \forall y \in (A ∖ m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
99		inundif	$⊢ (A \cap m) \cup (A ∖ m) = A$
100	99	raleqi	$⊢ \forall y \in ((A \cap m) \cup (A ∖ m)) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \leftrightarrow \forall y \in A h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
101		ralunb	$⊢ \forall y \in ((A \cap m) \cup (A ∖ m)) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \leftrightarrow (\forall y \in (A \cap m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \land \forall y \in (A ∖ m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)))$
102	100 101	bitr3i	$⊢ \forall y \in A h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \leftrightarrow (\forall y \in (A \cap m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \land \forall y \in (A ∖ m) h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)))$
103	81 98 102	sylanbrc	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \forall y \in A h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
104		ixpeq2	$⊢ \forall y \in A h (y) = ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) \to \underset{y \in A}{⨉} h (y) = \underset{y \in A}{⨉} ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
105	103 104	syl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \underset{y \in A}{⨉} h (y) = \underset{y \in A}{⨉} ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y))$
106		ixpiin	$⊢ A \cap m \neq \emptyset \to \underset{y \in A}{⨉} ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) = ⋂_{n \in A \cap m} \underset{y \in A}{⨉} if (y = n, h (n), ⋃ F (y))$
107	106	adantl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \underset{y \in A}{⨉} ⋂_{n \in A \cap m} if (y = n, h (n), ⋃ F (y)) = ⋂_{n \in A \cap m} \underset{y \in A}{⨉} if (y = n, h (n), ⋃ F (y))$
108	105 107	eqtrd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \underset{y \in A}{⨉} h (y) = ⋂_{n \in A \cap m} \underset{y \in A}{⨉} if (y = n, h (n), ⋃ F (y))$
109	39 53 108	3eqtr4rd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land A \cap m \neq \emptyset) \to \underset{y \in A}{⨉} h (y) = X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
110	25 109	pm2.61dane	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \underset{y \in A}{⨉} h (y) = X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
111		ixpexg	$⊢ \forall n \in A ⋃ F (n) \in V \to \underset{n \in A}{⨉} ⋃ F (n) \in V$
112		fvex	$⊢ F (n) \in V$
113	112	uniex	$⊢ ⋃ F (n) \in V$
114	113	a1i	$⊢ n \in A \to ⋃ F (n) \in V$
115	111 114	mprg	$⊢ \underset{n \in A}{⨉} ⋃ F (n) \in V$
116	2 115	eqeltri	$⊢ X \in V$
117	116	mptex	$⊢ (w \in X ⟼ w (n)) \in V$
118	117	cnvex	$⊢ {(w \in X ⟼ w (n))}^{-1} \in V$
119	118	imaex	$⊢ {(w \in X ⟼ w (n))}^{-1} [h (n)] \in V$
120	119	dfiin2	$⊢ ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = ⋂ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\}$
121		inteq	$⊢ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset \to ⋂ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = ⋂ \emptyset$
122	120 121	syl5eq	$⊢ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = ⋂ \emptyset$
123		int0	$⊢ ⋂ \emptyset = V$
124	122 123	eqtrdi	$⊢ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = V$
125	124	ineq2d	$⊢ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = X \cap V$
126		inv1	$⊢ X \cap V = X$
127	125 126	eqtrdi	$⊢ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = X$
128	127	adantl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset) \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = X$
129		snex	$⊢ \{X\} \in V$
130	1	ptbas	$⊢ (A \in V \land F : A ⟶ Top) \to B \in TopBases$
131	1 2	ptpjpre2	$⊢ ((A \in V \land F : A ⟶ Top) \land (k \in A \land u \in F (k))) \to {(w \in X ⟼ w (k))}^{-1} [u] \in B$
132	131	ralrimivva	$⊢ (A \in V \land F : A ⟶ Top) \to \forall k \in A \forall u \in F (k) {(w \in X ⟼ w (k))}^{-1} [u] \in B$
133		eqid	$⊢ (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
134	133	fmpox	$⊢ \forall k \in A \forall u \in F (k) {(w \in X ⟼ w (k))}^{-1} [u] \in B \leftrightarrow (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) : ⋃_{k \in A} (\{k\} \times F (k)) ⟶ B$
135	132 134	sylib	$⊢ (A \in V \land F : A ⟶ Top) \to (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) : ⋃_{k \in A} (\{k\} \times F (k)) ⟶ B$
136	135	frnd	$⊢ (A \in V \land F : A ⟶ Top) \to ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq B$
137	130 136	ssexd	$⊢ (A \in V \land F : A ⟶ Top) \to ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V$
138		unexg	$⊢ (\{X\} \in V \land ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V) \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V$
139	129 137 138	sylancr	$⊢ (A \in V \land F : A ⟶ Top) \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V$
140		ssfii	$⊢ \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
141	139 140	syl	$⊢ (A \in V \land F : A ⟶ Top) \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
142	141	ad2antrr	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
143		ssun1	$⊢ \{X\} \subseteq \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
144	116	snss	$⊢ X \in (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \leftrightarrow \{X\} \subseteq \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
145	143 144	mpbir	$⊢ X \in (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
146	145	a1i	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to X \in (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
147	142 146	sseldd	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to X \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
148	147	adantr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset) \to X \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
149	128 148	eqeltrd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} = \emptyset) \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
150	139	ad3antrrr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V$
151		nfv	$⊢ Ⅎ n (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y)))$
152		nfcv	$⊢ \underline{Ⅎ} n A$
153		nfcv	$⊢ \underline{Ⅎ} n F (k)$
154		nfixp1	$⊢ \underline{Ⅎ} n \underset{n \in A}{⨉} ⋃ F (n)$
155	2 154	nfcxfr	$⊢ \underline{Ⅎ} n X$
156		nfcv	$⊢ \underline{Ⅎ} n w (k)$
157	155 156	nfmpt	$⊢ \underline{Ⅎ} n (w \in X ⟼ w (k))$
158	157	nfcnv	$⊢ \underline{Ⅎ} n {(w \in X ⟼ w (k))}^{-1}$
159		nfcv	$⊢ \underline{Ⅎ} n u$
160	158 159	nfima	$⊢ \underline{Ⅎ} n {(w \in X ⟼ w (k))}^{-1} [u]$
161	152 153 160	nfmpo	$⊢ \underline{Ⅎ} n (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
162	161	nfrn	$⊢ \underline{Ⅎ} n ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
163	162	nfcri	$⊢ Ⅎ n z \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
164		df-ov	$⊢ n (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) h (n) = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) (⟨n, h (n)⟩)$
165	119	a1i	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to {(w \in X ⟼ w (n))}^{-1} [h (n)] \in V$
166		fveq2	$⊢ k = n \to w (k) = w (n)$
167	166	mpteq2dv	$⊢ k = n \to (w \in X ⟼ w (k)) = (w \in X ⟼ w (n))$
168	167	cnveqd	$⊢ k = n \to {(w \in X ⟼ w (k))}^{-1} = {(w \in X ⟼ w (n))}^{-1}$
169	168	imaeq1d	$⊢ k = n \to {(w \in X ⟼ w (k))}^{-1} [u] = {(w \in X ⟼ w (n))}^{-1} [u]$
170		imaeq2	$⊢ u = h (n) \to {(w \in X ⟼ w (n))}^{-1} [u] = {(w \in X ⟼ w (n))}^{-1} [h (n)]$
171	169 170	sylan9eq	$⊢ (k = n \land u = h (n)) \to {(w \in X ⟼ w (k))}^{-1} [u] = {(w \in X ⟼ w (n))}^{-1} [h (n)]$
172		fveq2	$⊢ k = n \to F (k) = F (n)$
173	171 172 133	ovmpox	$⊢ (n \in A \land h (n) \in F (n) \land {(w \in X ⟼ w (n))}^{-1} [h (n)] \in V) \to n (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) h (n) = {(w \in X ⟼ w (n))}^{-1} [h (n)]$
174	29 35 165 173	syl3anc	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to n (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) h (n) = {(w \in X ⟼ w (n))}^{-1} [h (n)]$
175	164 174	syl5eqr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) (⟨n, h (n)⟩) = {(w \in X ⟼ w (n))}^{-1} [h (n)]$
176	135	ad3antrrr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) : ⋃_{k \in A} (\{k\} \times F (k)) ⟶ B$
177	176	ffnd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) Fn ⋃_{k \in A} (\{k\} \times F (k))$
178		opeliunxp	$⊢ ⟨n, h (n)⟩ \in ⋃_{n \in A} (\{n\} \times F (n)) \leftrightarrow (n \in A \land h (n) \in F (n))$
179	29 35 178	sylanbrc	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to ⟨n, h (n)⟩ \in ⋃_{n \in A} (\{n\} \times F (n))$
180		sneq	$⊢ n = k \to \{n\} = \{k\}$
181		fveq2	$⊢ n = k \to F (n) = F (k)$
182	180 181	xpeq12d	$⊢ n = k \to \{n\} \times F (n) = \{k\} \times F (k)$
183	182	cbviunv	$⊢ ⋃_{n \in A} (\{n\} \times F (n)) = ⋃_{k \in A} (\{k\} \times F (k))$
184	179 183	eleqtrdi	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to ⟨n, h (n)⟩ \in ⋃_{k \in A} (\{k\} \times F (k))$
185		fnfvelrn	$⊢ ((k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) Fn ⋃_{k \in A} (\{k\} \times F (k)) \land ⟨n, h (n)⟩ \in ⋃_{k \in A} (\{k\} \times F (k))) \to (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) (⟨n, h (n)⟩) \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
186	177 184 185	syl2anc	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) (⟨n, h (n)⟩) \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
187	175 186	eqeltrrd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to {(w \in X ⟼ w (n))}^{-1} [h (n)] \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
188		eleq1	$⊢ z = {(w \in X ⟼ w (n))}^{-1} [h (n)] \to (z \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \leftrightarrow {(w \in X ⟼ w (n))}^{-1} [h (n)] \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
189	187 188	syl5ibrcom	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land n \in (A \cap m)) \to (z = {(w \in X ⟼ w (n))}^{-1} [h (n)] \to z \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
190	189	ex	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to (n \in (A \cap m) \to (z = {(w \in X ⟼ w (n))}^{-1} [h (n)] \to z \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])))$
191	151 163 190	rexlimd	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to (\exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)] \to z \in ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
192	191	abssdv	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \subseteq ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
193		ssun2	$⊢ ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
194	192 193	sstrdi	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \subseteq \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
195	194	adantr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \subseteq \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
196		simpr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset$
197		simplrl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to m \in Fin$
198		ssfi	$⊢ (m \in Fin \land A \cap m \subseteq m) \to A \cap m \in Fin$
199	197 84 198	sylancl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to A \cap m \in Fin$
200		abrexfi	$⊢ A \cap m \in Fin \to \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \in Fin$
201	199 200	syl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \in Fin$
202		elfir	$⊢ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V \land (\{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \subseteq \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \in Fin)) \to ⋂ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
203	150 195 196 201 202	syl13anc	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to ⋂ \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
204	120 203	eqeltrid	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
205		elssuni	$⊢ ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq ⋃ fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
206	204 205	syl	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq ⋃ fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
207		fiuni	$⊢ \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \in V \to ⋃ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) = ⋃ fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
208	139 207	syl	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) = ⋃ fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
209	116	pwid	$⊢ X \in 𝒫 X$
210	209	a1i	$⊢ (A \in V \land F : A ⟶ Top) \to X \in 𝒫 X$
211	210	snssd	$⊢ (A \in V \land F : A ⟶ Top) \to \{X\} \subseteq 𝒫 X$
212	1	ptuni2	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{n \in A}{⨉} ⋃ F (n) = ⋃ B$
213	2 212	syl5eq	$⊢ (A \in V \land F : A ⟶ Top) \to X = ⋃ B$
214		eqimss2	$⊢ X = ⋃ B \to ⋃ B \subseteq X$
215	213 214	syl	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ B \subseteq X$
216		sspwuni	$⊢ B \subseteq 𝒫 X \leftrightarrow ⋃ B \subseteq X$
217	215 216	sylibr	$⊢ (A \in V \land F : A ⟶ Top) \to B \subseteq 𝒫 X$
218	136 217	sstrd	$⊢ (A \in V \land F : A ⟶ Top) \to ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq 𝒫 X$
219	211 218	unssd	$⊢ (A \in V \land F : A ⟶ Top) \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq 𝒫 X$
220		sspwuni	$⊢ \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq 𝒫 X \leftrightarrow ⋃ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \subseteq X$
221	219 220	sylib	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \subseteq X$
222		elssuni	$⊢ X \in (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \to X \subseteq ⋃ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
223	145 222	mp1i	$⊢ (A \in V \land F : A ⟶ Top) \to X \subseteq ⋃ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
224	221 223	eqssd	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) = X$
225	208 224	eqtr3d	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) = X$
226	225	ad3antrrr	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to ⋃ fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) = X$
227	206 226	sseqtrd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \subseteq X$
228	227 52	sylib	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] = ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)]$
229	228 204	eqeltrd	$⊢ ((((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \land \{z \| \exists n \in (A \cap m) z = {(w \in X ⟼ w (n))}^{-1} [h (n)]\} \neq \emptyset) \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
230	149 229	pm2.61dane	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to X \cap ⋂_{n \in A \cap m} {(w \in X ⟼ w (n))}^{-1} [h (n)] \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
231	110 230	eqeltrd	$⊢ (((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \land (m \in Fin \land \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \underset{y \in A}{⨉} h (y) \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
232	231	rexlimdvaa	$⊢ ((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y))) \to (\exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y) \to \underset{y \in A}{⨉} h (y) \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])))$
233	232	impr	$⊢ ((A \in V \land F : A ⟶ Top) \land ((h Fn A \land \forall y \in A h (y) \in F (y)) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \underset{y \in A}{⨉} h (y) \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
234	4 233	sylan2b	$⊢ ((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to \underset{y \in A}{⨉} h (y) \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
235		eleq1	$⊢ s = \underset{y \in A}{⨉} h (y) \to (s \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \leftrightarrow \underset{y \in A}{⨉} h (y) \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])))$
236	234 235	syl5ibrcom	$⊢ ((A \in V \land F : A ⟶ Top) \land (h Fn A \land \forall y \in A h (y) \in F (y) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y))) \to (s = \underset{y \in A}{⨉} h (y) \to s \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])))$
237	236	expimpd	$⊢ (A \in V \land F : A ⟶ Top) \to (((h Fn A \land \forall y \in A h (y) \in F (y) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} h (y)) \to s \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])))$
238	237	exlimdv	$⊢ (A \in V \land F : A ⟶ Top) \to (\exists h ((h Fn A \land \forall y \in A h (y) \in F (y) \land \exists m \in Fin \forall y \in (A ∖ m) h (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} h (y)) \to s \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])))$
239	3 238	syl5bi	$⊢ (A \in V \land F : A ⟶ Top) \to (s \in B \to s \in fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])))$
240	239	ssrdv	$⊢ (A \in V \land F : A ⟶ Top) \to B \subseteq fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$
241	1	ptbasid	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{n \in A}{⨉} ⋃ F (n) \in B$
242	2 241	eqeltrid	$⊢ (A \in V \land F : A ⟶ Top) \to X \in B$
243	242	snssd	$⊢ (A \in V \land F : A ⟶ Top) \to \{X\} \subseteq B$
244	243 136	unssd	$⊢ (A \in V \land F : A ⟶ Top) \to \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq B$
245		fiss	$⊢ (B \in TopBases \land \{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]) \subseteq B) \to fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \subseteq fi (B)$
246	130 244 245	syl2anc	$⊢ (A \in V \land F : A ⟶ Top) \to fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \subseteq fi (B)$
247	1	ptbasin2	$⊢ (A \in V \land F : A ⟶ Top) \to fi (B) = B$
248	246 247	sseqtrd	$⊢ (A \in V \land F : A ⟶ Top) \to fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])) \subseteq B$
249	240 248	eqssd	$⊢ (A \in V \land F : A ⟶ Top) \to B = fi (\{X\} \cup ran (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u]))$

Metamath Proof Explorer

Theorem ptbasfi

Proof