ptcnplem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ptcnplem		Structured version Visualization version GIF version

Theorem ptcnplem 23683

Description: Lemma for ptcnp 23684. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)

**Hypotheses**
Ref	Expression
ptcnp.2	⊢ 𝐾 = (∏_t‘𝐹)
ptcnp.3	⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
ptcnp.4	⊢ (𝜑 → 𝐼 ∈ 𝑉)
ptcnp.5	⊢ (𝜑 → 𝐹:𝐼⟶Top)
ptcnp.6	⊢ (𝜑 → 𝐷 ∈ 𝑋)
ptcnp.7	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
ptcnplem.1	⊢ Ⅎ𝑘𝜓
ptcnplem.2	⊢ ((𝜑 ∧ 𝜓) → 𝐺 Fn 𝐼)
ptcnplem.3	⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘))
ptcnplem.4	⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ Fin)
ptcnplem.5	⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘))
ptcnplem.6	⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))

**Assertion**
Ref	Expression
ptcnplem	⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))

Distinct variable groups: 𝑧,𝐴 𝑥,𝑘,𝑧,𝐷 𝑘,𝐼,𝑥,𝑧 𝑥,𝐺,𝑧 𝑘,𝐽,𝑧 𝑧,𝐾 𝜑,𝑘,𝑥,𝑧 𝑘,𝐹,𝑥,𝑧 𝑘,𝑉,𝑥 𝑘,𝑊,𝑧 𝑘,𝑋,𝑥,𝑧 Allowed substitution hints: 𝜓(𝑥,𝑧,𝑘) 𝐴(𝑥,𝑘) 𝐺(𝑘) 𝐽(𝑥) 𝐾(𝑥,𝑘) 𝑉(𝑧) 𝑊(𝑥)

Proof of Theorem ptcnplem Dummy variables 𝑓 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptcnplem.4	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ Fin)
2		inss2 4191	. . . 4 ⊢ (𝐼 ∩ 𝑊) ⊆ 𝑊
3		ssfi 9143	. . . 4 ⊢ ((𝑊 ∈ Fin ∧ (𝐼 ∩ 𝑊) ⊆ 𝑊) → (𝐼 ∩ 𝑊) ∈ Fin)
4	1, 2, 3	sylancl 595	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝐼 ∩ 𝑊) ∈ Fin)
5		nfv 1936	. . . . 5 ⊢ Ⅎ𝑘𝜑
6		ptcnplem.1	. . . . 5 ⊢ Ⅎ𝑘𝜓
7	5, 6	nfan 1921	. . . 4 ⊢ Ⅎ𝑘(𝜑 ∧ 𝜓)
8		elinel1 4155	. . . . . 6 ⊢ (𝑘 ∈ (𝐼 ∩ 𝑊) → 𝑘 ∈ 𝐼)
9		ptcnp.7	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
10	9	adantlr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
11		ptcnplem.3	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘))
12		ptcnp.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
13	12	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ 𝑋)
14		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
15		ptcnp.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
16	15	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐽 ∈ (TopOn‘𝑋))
17		ptcnp.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:𝐼⟶Top)
18	17	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ Top)
19		toptopon2 22980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ Top ↔ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
20	18, 19	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
21		cnpf2 23312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
22	16, 20, 9, 21	syl3anc 1392	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
23		eqid 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴)
24	23	fmpt 7093	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
25	22, 24	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
26	25	r19.21bi 3256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ (𝐹‘𝑘))
27	23	fvmpt2 6989	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
28	14, 26, 27	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
29	28	an32s 662	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
30	29	mpteq2dva 5195	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ 𝐴))
31		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
32		ptcnp.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
33	32	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐼 ∈ 𝑉)
34	33	mptexd 7210	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
35		eqid 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
36	35	fvmpt2 6989	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
37	31, 34, 36	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
38	30, 37	eqtr4d 2802	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
39	38	ralrimiva 3156	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
40	39	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
41		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝐼
42		nffvmpt1 6880	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)
43	41, 42	nfmpt 5200	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
44		nffvmpt1 6880	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
45	43, 44	nfeq 2939	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
46		fveq2 6869	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
47	46	mpteq2dv 5196	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)))
48		fveq2 6869	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
49	47, 48	eqeq12d 2780	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ↔ (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
50	45, 49	rspc 3571	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
51	13, 40, 50	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
52		ptcnplem.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
53	51, 52	eqeltrd 2864	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
54	32	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ∈ 𝑉)
55		mptelixpg 8919	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
56	54, 55	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
57	53, 56	mpbid 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
58	57	r19.21bi 3256	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
59		cnpimaex 23318	. . . . . . 7 ⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷) ∧ (𝐺‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
60	10, 11, 58, 59	syl3anc 1392	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
61	8, 60	sylan2 602	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
62	61	ex 416	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∩ 𝑊) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))))
63	7, 62	ralrimi 3262	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
64		eleq2 2853	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (𝐷 ∈ 𝑢 ↔ 𝐷 ∈ (𝑓‘𝑘)))
65		imaeq2 6047	. . . . . 6 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) = ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)))
66	65	sseq1d 3969	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))
67	64, 66	anbi12d 641	. . . 4 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
68	67	ac6sfi 9230	. . 3 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
69	4, 63, 68	syl2anc 593	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
70	15	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
71		toponuni 22976	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
72	70, 71	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑋 = ∪ 𝐽)
73	72	ineq1d 4173	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) = (∪ 𝐽 ∩ ∩ ran 𝑓))
74		topontop 22975	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
75	15, 74	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
76	75	ad2antrr 736	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ Top)
77		frn 6701	. . . . . 6 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → ran 𝑓 ⊆ 𝐽)
78	77	ad2antrl 738	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ⊆ 𝐽)
79	4	adantr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝐼 ∩ 𝑊) ∈ Fin)
80		ffn 6693	. . . . . . . 8 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → 𝑓 Fn (𝐼 ∩ 𝑊))
81	80	ad2antrl 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓 Fn (𝐼 ∩ 𝑊))
82		dffn4 6786	. . . . . . 7 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) ↔ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
83	81, 82	sylib 220	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
84		fofi 9259	. . . . . 6 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
85	79, 83, 84	syl2anc 593	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ∈ Fin)
86		eqid 2764	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
87	86	rintopn 22971	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ∈ Fin) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
88	76, 78, 85, 87	syl3anc 1392	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
89	73, 88	eqeltrd 2864	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽)
90	12	ad2antrr 736	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ 𝑋)
91		simpl 486	. . . . . . 7 ⊢ ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → 𝐷 ∈ (𝑓‘𝑘))
92	91	ralimi 3101	. . . . . 6 ⊢ (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
93	92	ad2antll 739	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
94		eleq2 2853	. . . . . . 7 ⊢ (𝑧 = (𝑓‘𝑘) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑓‘𝑘)))
95	94	ralrn 7071	. . . . . 6 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
96	81, 95	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
97	93, 96	mpbird 259	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧)
98		elrint 4949	. . . 4 ⊢ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ↔ (𝐷 ∈ 𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧))
99	90, 97, 98	sylanbrc 592	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓))
100		nfv 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑓:(𝐼 ∩ 𝑊)⟶𝐽
101	7, 100	nfan 1921	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
102		funmpt 6561	. . . . . . . . . . . . 13 ⊢ Fun (𝑥 ∈ 𝑋 ↦ 𝐴)
103		simp-4l 792	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝜑)
104	103, 15	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
105		simpllr 785	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
106		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ (𝐼 ∩ 𝑊))
107	105, 106	ffvelcdmd 7068	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ 𝐽)
108		toponss 22989	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓‘𝑘) ∈ 𝐽) → (𝑓‘𝑘) ⊆ 𝑋)
109	104, 107, 108	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ 𝑋)
110	106	elin1d 4158	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ 𝐼)
111	103, 110, 25	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
112		dmmptg 6231	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
113	111, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
114	109, 113	sseqtrrd 3975	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴))
115		funimass4 6933	. . . . . . . . . . . . 13 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ 𝐴) ∧ (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
116	102, 114, 115	sylancr 596	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
117		nffvmpt1 6880	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡)
118	117	nfel1 2942	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)
119		nfv 1936	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)
120		fveq2 6869	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))
121	120	eleq1d 2849	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
122	118, 119, 121	cbvralw 3306	. . . . . . . . . . . 12 ⊢ (∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))
123	116, 122	bitrdi 289	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
124		inss1 4190	. . . . . . . . . . . . 13 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋
125		ssralv 4007	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋 → (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
126	124, 111, 125	mpsyl 68	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
127		inss2 4191	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ ∩ ran 𝑓
128	105, 80	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓 Fn (𝐼 ∩ 𝑊))
129		fnfvelrn 7063	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 Fn (𝐼 ∩ 𝑊) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → (𝑓‘𝑘) ∈ ran 𝑓)
130	128, 106, 129	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ ran 𝑓)
131		intss1 4923	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑘) ∈ ran 𝑓 → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
132	130, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
133	127, 132	sstrid 3949	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘))
134		ssralv 4007	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
135	133, 134	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
136		r19.26 3124	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) ↔ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
137		elinel1 4155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → 𝑥 ∈ 𝑋)
138	137, 27	sylan 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
139	138	eleq1d 2849	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ (𝐺‘𝑘)))
140	139	biimpd 231	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → 𝐴 ∈ (𝐺‘𝑘)))
141	140	expimpd 457	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → ((𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → 𝐴 ∈ (𝐺‘𝑘)))
142	141	ralimia 3098	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
143	136, 142	sylbir 237	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
144	126, 135, 143	syl6an 694	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
145	123, 144	sylbid 242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
146	145	expimpd 457	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
147	101, 146	ralimdaa 3265	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
148	147	impr 458	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
149		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
150		eldifi 4086	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐼 ∖ 𝑊) → 𝑘 ∈ 𝐼)
151	137, 26	sylan2 602	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → 𝐴 ∈ ∪ (𝐹‘𝑘))
152	151	ralrimiva 3156	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
153	149, 150, 152	syl2an 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
154		ptcnplem.5	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘))
155		eleq2 2853	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (𝐴 ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ ∪ (𝐹‘𝑘)))
156	155	ralbidv 3187	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
157	154, 156	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
158	153, 157	mpbird 259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
159	158	ex 416	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∖ 𝑊) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
160	7, 159	ralrimi 3262	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
161	160	adantr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
162		inundif 4435	. . . . . . . . 9 ⊢ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊)) = 𝐼
163	162	raleqi 3320	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
164		ralunb 4151	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
165	163, 164	bitr3i 279	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
166	148, 161, 165	sylanbrc 592	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
167		ralcom 3292	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
168	166, 167	sylibr 236	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))
169	32	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐼 ∈ 𝑉)
170		nffvmpt1 6880	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡)
171	170	nfel1 2942	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
172		nfv 1936	. . . . . . . 8 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
173		fveq2 6869	. . . . . . . . 9 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
174	173	eleq1d 2849	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
175	171, 172, 174	cbvralw 3306	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
176		mptexg 7207	. . . . . . . . . . 11 ⊢ (𝐼 ∈ 𝑉 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
177	137, 176, 36	syl2anr 606	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
178	177	eleq1d 2849	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
179		mptelixpg 8919	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
180	179	adantr 484	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
181	178, 180	bitrd 281	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
182	181	ralbidva 3185	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
183	175, 182	bitrid 285	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
184	169, 183	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
185	168, 184	mpbird 259	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
186		funmpt 6561	. . . . 5 ⊢ Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
187	32	mptexd 7210	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
188	187	ralrimivw 3160	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
189	188	ad2antrr 736	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
190		dmmptg 6231	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
191	189, 190	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
192	124, 191	sseqtrrid 3981	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)))
193		funimass4 6933	. . . . 5 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∧ (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
194	186, 192, 193	sylancr 596	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
195	185, 194	mpbird 259	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
196		eleq2 2853	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓)))
197		imaeq2 6047	. . . . . 6 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)))
198	197	sseq1d 3969	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
199	196, 198	anbi12d 641	. . . 4 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))))
200	199	rspcev 3583	. . 3 ⊢ (((𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
201	89, 99, 195, 200	syl12anc 847	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
202	69, 201	exlimddv 1957	1 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1562 ∃wex 1801 Ⅎwnf 1805 ∈ wcel 2144 ∀wral 3078 ∃wrex 3088 Vcvv 3456 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∪ cuni 4867 ∩ cint 4907 ↦ cmpt 5183 dom cdm 5649 ran crn 5650 “ cima 5652 Fun wfun 6517 Fn wfn 6518 ⟶wf 6519 –onto→wfo 6521 ‘cfv 6523 (class class class)co 7398 Xcixp 8881 Fincfn 8929 ∏_tcpt 17469 Topctop 22955 TopOnctopon 22972 CnP ccnp 23287

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3079 df-rex 3089 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-ov 7401 df-oprab 7402 df-mpo 7403 df-om 7849 df-1st 7972 df-2nd 7973 df-1o 8439 df-2o 8440 df-map 8812 df-ixp 8882 df-en 8930 df-dom 8931 df-fin 8933 df-top 22956 df-topon 22973 df-cnp 23290

This theorem is referenced by: ptcnp 23684

W3C validator