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 23608

Description: Lemma for ptcnp 23609. (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 4169	. . . 4 ⊢ (𝐼 ∩ 𝑊) ⊆ 𝑊
3		ssfi 9101	. . . 4 ⊢ ((𝑊 ∈ Fin ∧ (𝐼 ∩ 𝑊) ⊆ 𝑊) → (𝐼 ∩ 𝑊) ∈ Fin)
4	1, 2, 3	sylancl 593	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝐼 ∩ 𝑊) ∈ Fin)
5		nfv 1922	. . . . 5 ⊢ Ⅎ𝑘𝜑
6		ptcnplem.1	. . . . 5 ⊢ Ⅎ𝑘𝜓
7	5, 6	nfan 1907	. . . 4 ⊢ Ⅎ𝑘(𝜑 ∧ 𝜓)
8		elinel1 4133	. . . . . 6 ⊢ (𝑘 ∈ (𝐼 ∩ 𝑊) → 𝑘 ∈ 𝐼)
9		ptcnp.7	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
10	9	adantlr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
11		ptcnplem.3	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘))
12		ptcnp.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
13	12	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ 𝑋)
14		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
15		ptcnp.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
16	15	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐽 ∈ (TopOn‘𝑋))
17		ptcnp.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:𝐼⟶Top)
18	17	ffvelcdmda 7029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ Top)
19		toptopon2 22905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ Top ↔ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
20	18, 19	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
21		cnpf2 23237	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
22	16, 20, 9, 21	syl3anc 1380	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
23		eqid 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴)
24	23	fmpt 7055	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
25	22, 24	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
26	25	r19.21bi 3233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ (𝐹‘𝑘))
27	23	fvmpt2 6951	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
28	14, 26, 27	syl2anc 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
29	28	an32s 659	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
30	29	mpteq2dva 5168	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ 𝐴))
31		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
32		ptcnp.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
33	32	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐼 ∈ 𝑉)
34	33	mptexd 7172	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
35		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
36	35	fvmpt2 6951	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
37	31, 34, 36	syl2anc 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
38	30, 37	eqtr4d 2779	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
39	38	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
40	39	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
41		nfcv 2903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝐼
42		nffvmpt1 6842	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)
43	41, 42	nfmpt 5173	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
44		nffvmpt1 6842	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
45	43, 44	nfeq 2916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
46		fveq2 6831	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
47	46	mpteq2dv 5169	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)))
48		fveq2 6831	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
49	47, 48	eqeq12d 2757	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ↔ (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
50	45, 49	rspc 3550	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
51	13, 40, 50	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
52		ptcnplem.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
53	51, 52	eqeltrd 2841	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
54	32	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ∈ 𝑉)
55		mptelixpg 8877	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
56	54, 55	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
57	53, 56	mpbid 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
58	57	r19.21bi 3233	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
59		cnpimaex 23243	. . . . . . 7 ⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷) ∧ (𝐺‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
60	10, 11, 58, 59	syl3anc 1380	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
61	8, 60	sylan2 600	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
62	61	ex 414	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∩ 𝑊) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))))
63	7, 62	ralrimi 3239	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
64		eleq2 2830	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (𝐷 ∈ 𝑢 ↔ 𝐷 ∈ (𝑓‘𝑘)))
65		imaeq2 6015	. . . . . 6 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) = ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)))
66	65	sseq1d 3948	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))
67	64, 66	anbi12d 639	. . . 4 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
68	67	ac6sfi 9188	. . 3 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
69	4, 63, 68	syl2anc 591	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
70	15	ad2antrr 733	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
71		toponuni 22901	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
72	70, 71	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑋 = ∪ 𝐽)
73	72	ineq1d 4151	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) = (∪ 𝐽 ∩ ∩ ran 𝑓))
74		topontop 22900	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
75	15, 74	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
76	75	ad2antrr 733	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ Top)
77		frn 6666	. . . . . 6 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → ran 𝑓 ⊆ 𝐽)
78	77	ad2antrl 735	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ⊆ 𝐽)
79	4	adantr 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝐼 ∩ 𝑊) ∈ Fin)
80		ffn 6659	. . . . . . . 8 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → 𝑓 Fn (𝐼 ∩ 𝑊))
81	80	ad2antrl 735	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓 Fn (𝐼 ∩ 𝑊))
82		dffn4 6749	. . . . . . 7 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) ↔ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
83	81, 82	sylib 220	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
84		fofi 9217	. . . . . 6 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
85	79, 83, 84	syl2anc 591	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ∈ Fin)
86		eqid 2741	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
87	86	rintopn 22896	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ∈ Fin) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
88	76, 78, 85, 87	syl3anc 1380	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
89	73, 88	eqeltrd 2841	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽)
90	12	ad2antrr 733	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ 𝑋)
91		simpl 484	. . . . . . 7 ⊢ ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → 𝐷 ∈ (𝑓‘𝑘))
92	91	ralimi 3078	. . . . . 6 ⊢ (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
93	92	ad2antll 736	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
94		eleq2 2830	. . . . . . 7 ⊢ (𝑧 = (𝑓‘𝑘) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑓‘𝑘)))
95	94	ralrn 7033	. . . . . 6 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
96	81, 95	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
97	93, 96	mpbird 259	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧)
98		elrint 4922	. . . 4 ⊢ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ↔ (𝐷 ∈ 𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧))
99	90, 97, 98	sylanbrc 590	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓))
100		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑓:(𝐼 ∩ 𝑊)⟶𝐽
101	7, 100	nfan 1907	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
102		funmpt 6527	. . . . . . . . . . . . 13 ⊢ Fun (𝑥 ∈ 𝑋 ↦ 𝐴)
103		simp-4l 789	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝜑)
104	103, 15	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
105		simpllr 782	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
106		simplr 775	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ (𝐼 ∩ 𝑊))
107	105, 106	ffvelcdmd 7030	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ 𝐽)
108		toponss 22914	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓‘𝑘) ∈ 𝐽) → (𝑓‘𝑘) ⊆ 𝑋)
109	104, 107, 108	syl2anc 591	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ 𝑋)
110	106	elin1d 4136	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ 𝐼)
111	103, 110, 25	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
112		dmmptg 6197	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
113	111, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
114	109, 113	sseqtrrd 3954	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴))
115		funimass4 6895	. . . . . . . . . . . . 13 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ 𝐴) ∧ (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
116	102, 114, 115	sylancr 594	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
117		nffvmpt1 6842	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡)
118	117	nfel1 2919	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)
119		nfv 1922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)
120		fveq2 6831	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))
121	120	eleq1d 2826	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
122	118, 119, 121	cbvralw 3283	. . . . . . . . . . . 12 ⊢ (∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))
123	116, 122	bitrdi 289	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
124		inss1 4168	. . . . . . . . . . . . 13 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋
125		ssralv 3986	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋 → (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
126	124, 111, 125	mpsyl 68	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
127		inss2 4169	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ ∩ ran 𝑓
128	105, 80	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓 Fn (𝐼 ∩ 𝑊))
129		fnfvelrn 7025	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 Fn (𝐼 ∩ 𝑊) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → (𝑓‘𝑘) ∈ ran 𝑓)
130	128, 106, 129	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ ran 𝑓)
131		intss1 4896	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑘) ∈ ran 𝑓 → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
132	130, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
133	127, 132	sstrid 3928	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘))
134		ssralv 3986	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
135	133, 134	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
136		r19.26 3101	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) ↔ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
137		elinel1 4133	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → 𝑥 ∈ 𝑋)
138	137, 27	sylan 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
139	138	eleq1d 2826	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ (𝐺‘𝑘)))
140	139	biimpd 231	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → 𝐴 ∈ (𝐺‘𝑘)))
141	140	expimpd 455	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → ((𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → 𝐴 ∈ (𝐺‘𝑘)))
142	141	ralimia 3075	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
143	136, 142	sylbir 237	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
144	126, 135, 143	syl6an 691	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
145	123, 144	sylbid 242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
146	145	expimpd 455	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
147	101, 146	ralimdaa 3242	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
148	147	impr 456	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
149		simpl 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
150		eldifi 4064	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐼 ∖ 𝑊) → 𝑘 ∈ 𝐼)
151	137, 26	sylan2 600	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → 𝐴 ∈ ∪ (𝐹‘𝑘))
152	151	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
153	149, 150, 152	syl2an 603	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
154		ptcnplem.5	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘))
155		eleq2 2830	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (𝐴 ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ ∪ (𝐹‘𝑘)))
156	155	ralbidv 3164	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
157	154, 156	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
158	153, 157	mpbird 259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
159	158	ex 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∖ 𝑊) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
160	7, 159	ralrimi 3239	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
161	160	adantr 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
162		inundif 4410	. . . . . . . . 9 ⊢ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊)) = 𝐼
163	162	raleqi 3297	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
164		ralunb 4129	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
165	163, 164	bitr3i 279	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
166	148, 161, 165	sylanbrc 590	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
167		ralcom 3269	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
168	166, 167	sylibr 236	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))
169	32	ad2antrr 733	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐼 ∈ 𝑉)
170		nffvmpt1 6842	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡)
171	170	nfel1 2919	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
172		nfv 1922	. . . . . . . 8 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
173		fveq2 6831	. . . . . . . . 9 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
174	173	eleq1d 2826	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
175	171, 172, 174	cbvralw 3283	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
176		mptexg 7169	. . . . . . . . . . 11 ⊢ (𝐼 ∈ 𝑉 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
177	137, 176, 36	syl2anr 604	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
178	177	eleq1d 2826	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
179		mptelixpg 8877	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
180	179	adantr 482	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
181	178, 180	bitrd 281	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
182	181	ralbidva 3162	. . . . . . 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 6527	. . . . 5 ⊢ Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
187	32	mptexd 7172	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
188	187	ralrimivw 3137	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
189	188	ad2antrr 733	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
190		dmmptg 6197	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
191	189, 190	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
192	124, 191	sseqtrrid 3960	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)))
193		funimass4 6895	. . . . 5 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∧ (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
194	186, 192, 193	sylancr 594	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
195	185, 194	mpbird 259	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
196		eleq2 2830	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓)))
197		imaeq2 6015	. . . . . 6 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)))
198	197	sseq1d 3948	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
199	196, 198	anbi12d 639	. . . 4 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))))
200	199	rspcev 3562	. . 3 ⊢ (((𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
201	89, 99, 195, 200	syl12anc 843	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
202	69, 201	exlimddv 1943	1 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 397 = wceq 1548 ∃wex 1787 Ⅎwnf 1791 ∈ wcel 2121 ∀wral 3055 ∃wrex 3065 Vcvv 3433 ∖ cdif 3882 ∪ cun 3883 ∩ cin 3884 ⊆ wss 3885 ∪ cuni 4841 ∩ cint 4880 ↦ cmpt 5156 dom cdm 5621 ran crn 5622 “ cima 5624 Fun wfun 6483 Fn wfn 6484 ⟶wf 6485 –onto→wfo 6487 ‘cfv 6489 (class class class)co 7360 Xcixp 8839 Fincfn 8887 ∏_tcpt 17396 Topctop 22880 TopOnctopon 22897 CnP ccnp 23212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-ral 3056 df-rex 3066 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-iin 4927 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-1o 8399 df-2o 8400 df-map 8769 df-ixp 8840 df-en 8888 df-dom 8889 df-fin 8891 df-top 22881 df-topon 22898 df-cnp 23215

This theorem is referenced by: ptcnp 23609

W3C validator