ptcnplem

	Ref	Expression
Hypotheses	ptcnp.2	$⊢ K = \prod_{𝑡} (F)$
	ptcnp.3	$⊢ φ \to J \in TopOn (X)$
	ptcnp.4	$⊢ φ \to I \in V$
	ptcnp.5	$⊢ φ \to F : I ⟶ Top$
	ptcnp.6	$⊢ φ \to D \in X$
	ptcnp.7	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) \in (J CnP F (k)) (D)$
	ptcnplem.1	$⊢ Ⅎ k ψ$
	ptcnplem.2	$⊢ (φ \land ψ) \to G Fn I$
	ptcnplem.3	$⊢ ((φ \land ψ) \land k \in I) \to G (k) \in F (k)$
	ptcnplem.4	$⊢ (φ \land ψ) \to W \in Fin$
	ptcnplem.5	$⊢ ((φ \land ψ) \land k \in (I ∖ W)) \to G (k) = ⋃ F (k)$
	ptcnplem.6	$⊢ (φ \land ψ) \to (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{k \in I}{⨉} G (k)$
Assertion	ptcnplem	$⊢ (φ \land ψ) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} G (k))$

Proof

Step	Hyp	Ref	Expression
1		ptcnp.2	$⊢ K = \prod_{𝑡} (F)$
2		ptcnp.3	$⊢ φ \to J \in TopOn (X)$
3		ptcnp.4	$⊢ φ \to I \in V$
4		ptcnp.5	$⊢ φ \to F : I ⟶ Top$
5		ptcnp.6	$⊢ φ \to D \in X$
6		ptcnp.7	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) \in (J CnP F (k)) (D)$
7		ptcnplem.1	$⊢ Ⅎ k ψ$
8		ptcnplem.2	$⊢ (φ \land ψ) \to G Fn I$
9		ptcnplem.3	$⊢ ((φ \land ψ) \land k \in I) \to G (k) \in F (k)$
10		ptcnplem.4	$⊢ (φ \land ψ) \to W \in Fin$
11		ptcnplem.5	$⊢ ((φ \land ψ) \land k \in (I ∖ W)) \to G (k) = ⋃ F (k)$
12		ptcnplem.6	$⊢ (φ \land ψ) \to (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{k \in I}{⨉} G (k)$
13		inss2	$⊢ I \cap W \subseteq W$
14		ssfi	$⊢ (W \in Fin \land I \cap W \subseteq W) \to I \cap W \in Fin$
15	10 13 14	sylancl	$⊢ (φ \land ψ) \to I \cap W \in Fin$
16		nfv	$⊢ Ⅎ k φ$
17	16 7	nfan	$⊢ Ⅎ k (φ \land ψ)$
18		elinel1	$⊢ k \in (I \cap W) \to k \in I$
19	6	adantlr	$⊢ ((φ \land ψ) \land k \in I) \to (x \in X ⟼ A) \in (J CnP F (k)) (D)$
20	5	adantr	$⊢ (φ \land ψ) \to D \in X$
21		simpr	$⊢ ((φ \land k \in I) \land x \in X) \to x \in X$
22	2	adantr	$⊢ (φ \land k \in I) \to J \in TopOn (X)$
23	4	ffvelcdmda	$⊢ (φ \land k \in I) \to F (k) \in Top$
24		toptopon2	$⊢ F (k) \in Top \leftrightarrow F (k) \in TopOn (⋃ F (k))$
25	23 24	sylib	$⊢ (φ \land k \in I) \to F (k) \in TopOn (⋃ F (k))$
26		cnpf2	$⊢ (J \in TopOn (X) \land F (k) \in TopOn (⋃ F (k)) \land (x \in X ⟼ A) \in (J CnP F (k)) (D)) \to (x \in X ⟼ A) : X ⟶ ⋃ F (k)$
27	22 25 6 26	syl3anc	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) : X ⟶ ⋃ F (k)$
28		eqid	$⊢ (x \in X ⟼ A) = (x \in X ⟼ A)$
29	28	fmpt	$⊢ \forall x \in X A \in ⋃ F (k) \leftrightarrow (x \in X ⟼ A) : X ⟶ ⋃ F (k)$
30	27 29	sylibr	$⊢ (φ \land k \in I) \to \forall x \in X A \in ⋃ F (k)$
31	30	r19.21bi	$⊢ ((φ \land k \in I) \land x \in X) \to A \in ⋃ F (k)$
32	28	fvmpt2	$⊢ (x \in X \land A \in ⋃ F (k)) \to (x \in X ⟼ A) (x) = A$
33	21 31 32	syl2anc	$⊢ ((φ \land k \in I) \land x \in X) \to (x \in X ⟼ A) (x) = A$
34	33	an32s	$⊢ ((φ \land x \in X) \land k \in I) \to (x \in X ⟼ A) (x) = A$
35	34	mpteq2dva	$⊢ (φ \land x \in X) \to (k \in I ⟼ (x \in X ⟼ A) (x)) = (k \in I ⟼ A)$
36		simpr	$⊢ (φ \land x \in X) \to x \in X$
37	3	adantr	$⊢ (φ \land x \in X) \to I \in V$
38	37	mptexd	$⊢ (φ \land x \in X) \to (k \in I ⟼ A) \in V$
39		eqid	$⊢ (x \in X ⟼ (k \in I ⟼ A)) = (x \in X ⟼ (k \in I ⟼ A))$
40	39	fvmpt2	$⊢ (x \in X \land (k \in I ⟼ A) \in V) \to (x \in X ⟼ (k \in I ⟼ A)) (x) = (k \in I ⟼ A)$
41	36 38 40	syl2anc	$⊢ (φ \land x \in X) \to (x \in X ⟼ (k \in I ⟼ A)) (x) = (k \in I ⟼ A)$
42	35 41	eqtr4d	$⊢ (φ \land x \in X) \to (k \in I ⟼ (x \in X ⟼ A) (x)) = (x \in X ⟼ (k \in I ⟼ A)) (x)$
43	42	ralrimiva	$⊢ φ \to \forall x \in X (k \in I ⟼ (x \in X ⟼ A) (x)) = (x \in X ⟼ (k \in I ⟼ A)) (x)$
44	43	adantr	$⊢ (φ \land ψ) \to \forall x \in X (k \in I ⟼ (x \in X ⟼ A) (x)) = (x \in X ⟼ (k \in I ⟼ A)) (x)$
45		nfcv	$⊢ \underline{Ⅎ} x I$
46		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ A) (D)$
47	45 46	nfmpt	$⊢ \underline{Ⅎ} x (k \in I ⟼ (x \in X ⟼ A) (D))$
48		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ (k \in I ⟼ A)) (D)$
49	47 48	nfeq	$⊢ Ⅎ x (k \in I ⟼ (x \in X ⟼ A) (D)) = (x \in X ⟼ (k \in I ⟼ A)) (D)$
50		fveq2	$⊢ x = D \to (x \in X ⟼ A) (x) = (x \in X ⟼ A) (D)$
51	50	mpteq2dv	$⊢ x = D \to (k \in I ⟼ (x \in X ⟼ A) (x)) = (k \in I ⟼ (x \in X ⟼ A) (D))$
52		fveq2	$⊢ x = D \to (x \in X ⟼ (k \in I ⟼ A)) (x) = (x \in X ⟼ (k \in I ⟼ A)) (D)$
53	51 52	eqeq12d	$⊢ x = D \to ((k \in I ⟼ (x \in X ⟼ A) (x)) = (x \in X ⟼ (k \in I ⟼ A)) (x) \leftrightarrow (k \in I ⟼ (x \in X ⟼ A) (D)) = (x \in X ⟼ (k \in I ⟼ A)) (D))$
54	49 53	rspc	$⊢ D \in X \to (\forall x \in X (k \in I ⟼ (x \in X ⟼ A) (x)) = (x \in X ⟼ (k \in I ⟼ A)) (x) \to (k \in I ⟼ (x \in X ⟼ A) (D)) = (x \in X ⟼ (k \in I ⟼ A)) (D))$
55	20 44 54	sylc	$⊢ (φ \land ψ) \to (k \in I ⟼ (x \in X ⟼ A) (D)) = (x \in X ⟼ (k \in I ⟼ A)) (D)$
56	55 12	eqeltrd	$⊢ (φ \land ψ) \to (k \in I ⟼ (x \in X ⟼ A) (D)) \in \underset{k \in I}{⨉} G (k)$
57	3	adantr	$⊢ (φ \land ψ) \to I \in V$
58		mptelixpg	$⊢ I \in V \to ((k \in I ⟼ (x \in X ⟼ A) (D)) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall k \in I (x \in X ⟼ A) (D) \in G (k))$
59	57 58	syl	$⊢ (φ \land ψ) \to ((k \in I ⟼ (x \in X ⟼ A) (D)) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall k \in I (x \in X ⟼ A) (D) \in G (k))$
60	56 59	mpbid	$⊢ (φ \land ψ) \to \forall k \in I (x \in X ⟼ A) (D) \in G (k)$
61	60	r19.21bi	$⊢ ((φ \land ψ) \land k \in I) \to (x \in X ⟼ A) (D) \in G (k)$
62		cnpimaex	$⊢ ((x \in X ⟼ A) \in (J CnP F (k)) (D) \land G (k) \in F (k) \land (x \in X ⟼ A) (D) \in G (k)) \to \exists u \in J (D \in u \land (x \in X ⟼ A) [u] \subseteq G (k))$
63	19 9 61 62	syl3anc	$⊢ ((φ \land ψ) \land k \in I) \to \exists u \in J (D \in u \land (x \in X ⟼ A) [u] \subseteq G (k))$
64	18 63	sylan2	$⊢ ((φ \land ψ) \land k \in (I \cap W)) \to \exists u \in J (D \in u \land (x \in X ⟼ A) [u] \subseteq G (k))$
65	64	ex	$⊢ (φ \land ψ) \to (k \in (I \cap W) \to \exists u \in J (D \in u \land (x \in X ⟼ A) [u] \subseteq G (k)))$
66	17 65	ralrimi	$⊢ (φ \land ψ) \to \forall k \in (I \cap W) \exists u \in J (D \in u \land (x \in X ⟼ A) [u] \subseteq G (k))$
67		eleq2	$⊢ u = f (k) \to (D \in u \leftrightarrow D \in f (k))$
68		imaeq2	$⊢ u = f (k) \to (x \in X ⟼ A) [u] = (x \in X ⟼ A) [f (k)]$
69	68	sseq1d	$⊢ u = f (k) \to ((x \in X ⟼ A) [u] \subseteq G (k) \leftrightarrow (x \in X ⟼ A) [f (k)] \subseteq G (k))$
70	67 69	anbi12d	$⊢ u = f (k) \to ((D \in u \land (x \in X ⟼ A) [u] \subseteq G (k)) \leftrightarrow (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))$
71	70	ac6sfi	$⊢ (I \cap W \in Fin \land \forall k \in (I \cap W) \exists u \in J (D \in u \land (x \in X ⟼ A) [u] \subseteq G (k))) \to \exists f (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))$
72	15 66 71	syl2anc	$⊢ (φ \land ψ) \to \exists f (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))$
73	2	ad2antrr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to J \in TopOn (X)$
74		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
75	73 74	syl	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to X = ⋃ J$
76	75	ineq1d	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to X \cap ⋂ ran f = ⋃ J \cap ⋂ ran f$
77		topontop	$⊢ J \in TopOn (X) \to J \in Top$
78	2 77	syl	$⊢ φ \to J \in Top$
79	78	ad2antrr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to J \in Top$
80		frn	$⊢ f : I \cap W ⟶ J \to ran f \subseteq J$
81	80	ad2antrl	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to ran f \subseteq J$
82	15	adantr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to I \cap W \in Fin$
83		ffn	$⊢ f : I \cap W ⟶ J \to f Fn (I \cap W)$
84	83	ad2antrl	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to f Fn (I \cap W)$
85		dffn4	$⊢ f Fn (I \cap W) \leftrightarrow f : I \cap W \underset{onto}{⟶} ran f$
86	84 85	sylib	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to f : I \cap W \underset{onto}{⟶} ran f$
87		fofi	$⊢ (I \cap W \in Fin \land f : I \cap W \underset{onto}{⟶} ran f) \to ran f \in Fin$
88	82 86 87	syl2anc	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to ran f \in Fin$
89		eqid	$⊢ ⋃ J = ⋃ J$
90	89	rintopn	$⊢ (J \in Top \land ran f \subseteq J \land ran f \in Fin) \to ⋃ J \cap ⋂ ran f \in J$
91	79 81 88 90	syl3anc	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to ⋃ J \cap ⋂ ran f \in J$
92	76 91	eqeltrd	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to X \cap ⋂ ran f \in J$
93	5	ad2antrr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to D \in X$
94		simpl	$⊢ (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)) \to D \in f (k)$
95	94	ralimi	$⊢ \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)) \to \forall k \in (I \cap W) D \in f (k)$
96	95	ad2antll	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall k \in (I \cap W) D \in f (k)$
97		eleq2	$⊢ z = f (k) \to (D \in z \leftrightarrow D \in f (k))$
98	97	ralrn	$⊢ f Fn (I \cap W) \to (\forall z \in ran f D \in z \leftrightarrow \forall k \in (I \cap W) D \in f (k))$
99	84 98	syl	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to (\forall z \in ran f D \in z \leftrightarrow \forall k \in (I \cap W) D \in f (k))$
100	96 99	mpbird	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall z \in ran f D \in z$
101		elrint	$⊢ D \in (X \cap ⋂ ran f) \leftrightarrow (D \in X \land \forall z \in ran f D \in z)$
102	93 100 101	sylanbrc	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to D \in (X \cap ⋂ ran f)$
103		nfv	$⊢ Ⅎ k f : I \cap W ⟶ J$
104	17 103	nfan	$⊢ Ⅎ k ((φ \land ψ) \land f : I \cap W ⟶ J)$
105		funmpt	$⊢ Fun (x \in X ⟼ A)$
106		simp-4l	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to φ$
107	106 2	syl	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to J \in TopOn (X)$
108		simpllr	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to f : I \cap W ⟶ J$
109		simplr	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to k \in (I \cap W)$
110	108 109	ffvelcdmd	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to f (k) \in J$
111		toponss	$⊢ (J \in TopOn (X) \land f (k) \in J) \to f (k) \subseteq X$
112	107 110 111	syl2anc	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to f (k) \subseteq X$
113	109	elin1d	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to k \in I$
114	106 113 30	syl2anc	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to \forall x \in X A \in ⋃ F (k)$
115		dmmptg	$⊢ \forall x \in X A \in ⋃ F (k) \to dom (x \in X ⟼ A) = X$
116	114 115	syl	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to dom (x \in X ⟼ A) = X$
117	112 116	sseqtrrd	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to f (k) \subseteq dom (x \in X ⟼ A)$
118		funimass4	$⊢ (Fun (x \in X ⟼ A) \land f (k) \subseteq dom (x \in X ⟼ A)) \to ((x \in X ⟼ A) [f (k)] \subseteq G (k) \leftrightarrow \forall t \in f (k) (x \in X ⟼ A) (t) \in G (k))$
119	105 117 118	sylancr	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to ((x \in X ⟼ A) [f (k)] \subseteq G (k) \leftrightarrow \forall t \in f (k) (x \in X ⟼ A) (t) \in G (k))$
120		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ A) (t)$
121	120	nfel1	$⊢ Ⅎ x (x \in X ⟼ A) (t) \in G (k)$
122		nfv	$⊢ Ⅎ t (x \in X ⟼ A) (x) \in G (k)$
123		fveq2	$⊢ t = x \to (x \in X ⟼ A) (t) = (x \in X ⟼ A) (x)$
124	123	eleq1d	$⊢ t = x \to ((x \in X ⟼ A) (t) \in G (k) \leftrightarrow (x \in X ⟼ A) (x) \in G (k))$
125	121 122 124	cbvralw	$⊢ \forall t \in f (k) (x \in X ⟼ A) (t) \in G (k) \leftrightarrow \forall x \in f (k) (x \in X ⟼ A) (x) \in G (k)$
126	119 125	bitrdi	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to ((x \in X ⟼ A) [f (k)] \subseteq G (k) \leftrightarrow \forall x \in f (k) (x \in X ⟼ A) (x) \in G (k))$
127		inss1	$⊢ X \cap ⋂ ran f \subseteq X$
128		ssralv	$⊢ X \cap ⋂ ran f \subseteq X \to (\forall x \in X A \in ⋃ F (k) \to \forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k))$
129	127 114 128	mpsyl	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to \forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k)$
130		inss2	$⊢ X \cap ⋂ ran f \subseteq ⋂ ran f$
131	108 83	syl	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to f Fn (I \cap W)$
132		fnfvelrn	$⊢ (f Fn (I \cap W) \land k \in (I \cap W)) \to f (k) \in ran f$
133	131 109 132	syl2anc	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to f (k) \in ran f$
134		intss1	$⊢ f (k) \in ran f \to ⋂ ran f \subseteq f (k)$
135	133 134	syl	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to ⋂ ran f \subseteq f (k)$
136	130 135	sstrid	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to X \cap ⋂ ran f \subseteq f (k)$
137		ssralv	$⊢ X \cap ⋂ ran f \subseteq f (k) \to (\forall x \in f (k) (x \in X ⟼ A) (x) \in G (k) \to \forall x \in (X \cap ⋂ ran f) (x \in X ⟼ A) (x) \in G (k))$
138	136 137	syl	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to (\forall x \in f (k) (x \in X ⟼ A) (x) \in G (k) \to \forall x \in (X \cap ⋂ ran f) (x \in X ⟼ A) (x) \in G (k))$
139		r19.26	$⊢ \forall x \in (X \cap ⋂ ran f) (A \in ⋃ F (k) \land (x \in X ⟼ A) (x) \in G (k)) \leftrightarrow (\forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k) \land \forall x \in (X \cap ⋂ ran f) (x \in X ⟼ A) (x) \in G (k))$
140		elinel1	$⊢ x \in (X \cap ⋂ ran f) \to x \in X$
141	140 32	sylan	$⊢ (x \in (X \cap ⋂ ran f) \land A \in ⋃ F (k)) \to (x \in X ⟼ A) (x) = A$
142	141	eleq1d	$⊢ (x \in (X \cap ⋂ ran f) \land A \in ⋃ F (k)) \to ((x \in X ⟼ A) (x) \in G (k) \leftrightarrow A \in G (k))$
143	142	biimpd	$⊢ (x \in (X \cap ⋂ ran f) \land A \in ⋃ F (k)) \to ((x \in X ⟼ A) (x) \in G (k) \to A \in G (k))$
144	143	expimpd	$⊢ x \in (X \cap ⋂ ran f) \to ((A \in ⋃ F (k) \land (x \in X ⟼ A) (x) \in G (k)) \to A \in G (k))$
145	144	ralimia	$⊢ \forall x \in (X \cap ⋂ ran f) (A \in ⋃ F (k) \land (x \in X ⟼ A) (x) \in G (k)) \to \forall x \in (X \cap ⋂ ran f) A \in G (k)$
146	139 145	sylbir	$⊢ (\forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k) \land \forall x \in (X \cap ⋂ ran f) (x \in X ⟼ A) (x) \in G (k)) \to \forall x \in (X \cap ⋂ ran f) A \in G (k)$
147	129 138 146	syl6an	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to (\forall x \in f (k) (x \in X ⟼ A) (x) \in G (k) \to \forall x \in (X \cap ⋂ ran f) A \in G (k))$
148	126 147	sylbid	$⊢ ((((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \land D \in f (k)) \to ((x \in X ⟼ A) [f (k)] \subseteq G (k) \to \forall x \in (X \cap ⋂ ran f) A \in G (k))$
149	148	expimpd	$⊢ (((φ \land ψ) \land f : I \cap W ⟶ J) \land k \in (I \cap W)) \to ((D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)) \to \forall x \in (X \cap ⋂ ran f) A \in G (k))$
150	104 149	ralimdaa	$⊢ ((φ \land ψ) \land f : I \cap W ⟶ J) \to (\forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)) \to \forall k \in (I \cap W) \forall x \in (X \cap ⋂ ran f) A \in G (k))$
151	150	impr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall k \in (I \cap W) \forall x \in (X \cap ⋂ ran f) A \in G (k)$
152		simpl	$⊢ (φ \land ψ) \to φ$
153		eldifi	$⊢ k \in (I ∖ W) \to k \in I$
154	140 31	sylan2	$⊢ ((φ \land k \in I) \land x \in (X \cap ⋂ ran f)) \to A \in ⋃ F (k)$
155	154	ralrimiva	$⊢ (φ \land k \in I) \to \forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k)$
156	152 153 155	syl2an	$⊢ ((φ \land ψ) \land k \in (I ∖ W)) \to \forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k)$
157		eleq2	$⊢ G (k) = ⋃ F (k) \to (A \in G (k) \leftrightarrow A \in ⋃ F (k))$
158	157	ralbidv	$⊢ G (k) = ⋃ F (k) \to (\forall x \in (X \cap ⋂ ran f) A \in G (k) \leftrightarrow \forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k))$
159	11 158	syl	$⊢ ((φ \land ψ) \land k \in (I ∖ W)) \to (\forall x \in (X \cap ⋂ ran f) A \in G (k) \leftrightarrow \forall x \in (X \cap ⋂ ran f) A \in ⋃ F (k))$
160	156 159	mpbird	$⊢ ((φ \land ψ) \land k \in (I ∖ W)) \to \forall x \in (X \cap ⋂ ran f) A \in G (k)$
161	160	ex	$⊢ (φ \land ψ) \to (k \in (I ∖ W) \to \forall x \in (X \cap ⋂ ran f) A \in G (k))$
162	17 161	ralrimi	$⊢ (φ \land ψ) \to \forall k \in (I ∖ W) \forall x \in (X \cap ⋂ ran f) A \in G (k)$
163	162	adantr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall k \in (I ∖ W) \forall x \in (X \cap ⋂ ran f) A \in G (k)$
164		inundif	$⊢ (I \cap W) \cup (I ∖ W) = I$
165	164	raleqi	$⊢ \forall k \in ((I \cap W) \cup (I ∖ W)) \forall x \in (X \cap ⋂ ran f) A \in G (k) \leftrightarrow \forall k \in I \forall x \in (X \cap ⋂ ran f) A \in G (k)$
166		ralunb	$⊢ \forall k \in ((I \cap W) \cup (I ∖ W)) \forall x \in (X \cap ⋂ ran f) A \in G (k) \leftrightarrow (\forall k \in (I \cap W) \forall x \in (X \cap ⋂ ran f) A \in G (k) \land \forall k \in (I ∖ W) \forall x \in (X \cap ⋂ ran f) A \in G (k))$
167	165 166	bitr3i	$⊢ \forall k \in I \forall x \in (X \cap ⋂ ran f) A \in G (k) \leftrightarrow (\forall k \in (I \cap W) \forall x \in (X \cap ⋂ ran f) A \in G (k) \land \forall k \in (I ∖ W) \forall x \in (X \cap ⋂ ran f) A \in G (k))$
168	151 163 167	sylanbrc	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall k \in I \forall x \in (X \cap ⋂ ran f) A \in G (k)$
169		ralcom	$⊢ \forall x \in (X \cap ⋂ ran f) \forall k \in I A \in G (k) \leftrightarrow \forall k \in I \forall x \in (X \cap ⋂ ran f) A \in G (k)$
170	168 169	sylibr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall x \in (X \cap ⋂ ran f) \forall k \in I A \in G (k)$
171	3	ad2antrr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to I \in V$
172		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ (k \in I ⟼ A)) (t)$
173	172	nfel1	$⊢ Ⅎ x (x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k)$
174		nfv	$⊢ Ⅎ t (x \in X ⟼ (k \in I ⟼ A)) (x) \in \underset{k \in I}{⨉} G (k)$
175		fveq2	$⊢ t = x \to (x \in X ⟼ (k \in I ⟼ A)) (t) = (x \in X ⟼ (k \in I ⟼ A)) (x)$
176	175	eleq1d	$⊢ t = x \to ((x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k) \leftrightarrow (x \in X ⟼ (k \in I ⟼ A)) (x) \in \underset{k \in I}{⨉} G (k))$
177	173 174 176	cbvralw	$⊢ \forall t \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall x \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (x) \in \underset{k \in I}{⨉} G (k)$
178		mptexg	$⊢ I \in V \to (k \in I ⟼ A) \in V$
179	140 178 40	syl2anr	$⊢ (I \in V \land x \in (X \cap ⋂ ran f)) \to (x \in X ⟼ (k \in I ⟼ A)) (x) = (k \in I ⟼ A)$
180	179	eleq1d	$⊢ (I \in V \land x \in (X \cap ⋂ ran f)) \to ((x \in X ⟼ (k \in I ⟼ A)) (x) \in \underset{k \in I}{⨉} G (k) \leftrightarrow (k \in I ⟼ A) \in \underset{k \in I}{⨉} G (k))$
181		mptelixpg	$⊢ I \in V \to ((k \in I ⟼ A) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall k \in I A \in G (k))$
182	181	adantr	$⊢ (I \in V \land x \in (X \cap ⋂ ran f)) \to ((k \in I ⟼ A) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall k \in I A \in G (k))$
183	180 182	bitrd	$⊢ (I \in V \land x \in (X \cap ⋂ ran f)) \to ((x \in X ⟼ (k \in I ⟼ A)) (x) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall k \in I A \in G (k))$
184	183	ralbidva	$⊢ I \in V \to (\forall x \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (x) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall x \in (X \cap ⋂ ran f) \forall k \in I A \in G (k))$
185	177 184	bitrid	$⊢ I \in V \to (\forall t \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall x \in (X \cap ⋂ ran f) \forall k \in I A \in G (k))$
186	171 185	syl	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to (\forall t \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k) \leftrightarrow \forall x \in (X \cap ⋂ ran f) \forall k \in I A \in G (k))$
187	170 186	mpbird	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall t \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k)$
188		funmpt	$⊢ Fun (x \in X ⟼ (k \in I ⟼ A))$
189	3	mptexd	$⊢ φ \to (k \in I ⟼ A) \in V$
190	189	ralrimivw	$⊢ φ \to \forall x \in X (k \in I ⟼ A) \in V$
191	190	ad2antrr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \forall x \in X (k \in I ⟼ A) \in V$
192		dmmptg	$⊢ \forall x \in X (k \in I ⟼ A) \in V \to dom (x \in X ⟼ (k \in I ⟼ A)) = X$
193	191 192	syl	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to dom (x \in X ⟼ (k \in I ⟼ A)) = X$
194	127 193	sseqtrrid	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to X \cap ⋂ ran f \subseteq dom (x \in X ⟼ (k \in I ⟼ A))$
195		funimass4	$⊢ (Fun (x \in X ⟼ (k \in I ⟼ A)) \land X \cap ⋂ ran f \subseteq dom (x \in X ⟼ (k \in I ⟼ A))) \to ((x \in X ⟼ (k \in I ⟼ A)) [X \cap ⋂ ran f] \subseteq \underset{k \in I}{⨉} G (k) \leftrightarrow \forall t \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k))$
196	188 194 195	sylancr	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to ((x \in X ⟼ (k \in I ⟼ A)) [X \cap ⋂ ran f] \subseteq \underset{k \in I}{⨉} G (k) \leftrightarrow \forall t \in (X \cap ⋂ ran f) (x \in X ⟼ (k \in I ⟼ A)) (t) \in \underset{k \in I}{⨉} G (k))$
197	187 196	mpbird	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to (x \in X ⟼ (k \in I ⟼ A)) [X \cap ⋂ ran f] \subseteq \underset{k \in I}{⨉} G (k)$
198		eleq2	$⊢ z = X \cap ⋂ ran f \to (D \in z \leftrightarrow D \in (X \cap ⋂ ran f))$
199		imaeq2	$⊢ z = X \cap ⋂ ran f \to (x \in X ⟼ (k \in I ⟼ A)) [z] = (x \in X ⟼ (k \in I ⟼ A)) [X \cap ⋂ ran f]$
200	199	sseq1d	$⊢ z = X \cap ⋂ ran f \to ((x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} G (k) \leftrightarrow (x \in X ⟼ (k \in I ⟼ A)) [X \cap ⋂ ran f] \subseteq \underset{k \in I}{⨉} G (k))$
201	198 200	anbi12d	$⊢ z = X \cap ⋂ ran f \to ((D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} G (k)) \leftrightarrow (D \in (X \cap ⋂ ran f) \land (x \in X ⟼ (k \in I ⟼ A)) [X \cap ⋂ ran f] \subseteq \underset{k \in I}{⨉} G (k)))$
202	201	rspcev	$⊢ (X \cap ⋂ ran f \in J \land (D \in (X \cap ⋂ ran f) \land (x \in X ⟼ (k \in I ⟼ A)) [X \cap ⋂ ran f] \subseteq \underset{k \in I}{⨉} G (k))) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} G (k))$
203	92 102 197 202	syl12anc	$⊢ ((φ \land ψ) \land (f : I \cap W ⟶ J \land \forall k \in (I \cap W) (D \in f (k) \land (x \in X ⟼ A) [f (k)] \subseteq G (k)))) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} G (k))$
204	72 203	exlimddv	$⊢ (φ \land ψ) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} G (k))$

Metamath Proof Explorer

Theorem ptcnplem

Proof