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 23508

Description: Lemma for ptcnp 23509. (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 4201	. . . 4 ⊢ (𝐼 ∩ 𝑊) ⊆ 𝑊
3		ssfi 9137	. . . 4 ⊢ ((𝑊 ∈ Fin ∧ (𝐼 ∩ 𝑊) ⊆ 𝑊) → (𝐼 ∩ 𝑊) ∈ Fin)
4	1, 2, 3	sylancl 586	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝐼 ∩ 𝑊) ∈ Fin)
5		nfv 1914	. . . . 5 ⊢ Ⅎ𝑘𝜑
6		ptcnplem.1	. . . . 5 ⊢ Ⅎ𝑘𝜓
7	5, 6	nfan 1899	. . . 4 ⊢ Ⅎ𝑘(𝜑 ∧ 𝜓)
8		elinel1 4164	. . . . . 6 ⊢ (𝑘 ∈ (𝐼 ∩ 𝑊) → 𝑘 ∈ 𝐼)
9		ptcnp.7	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
10	9	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
11		ptcnplem.3	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘))
12		ptcnp.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
13	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ 𝑋)
14		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
15		ptcnp.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
16	15	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐽 ∈ (TopOn‘𝑋))
17		ptcnp.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:𝐼⟶Top)
18	17	ffvelcdmda 7056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ Top)
19		toptopon2 22805	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ Top ↔ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
20	18, 19	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
21		cnpf2 23137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
22	16, 20, 9, 21	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
23		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴)
24	23	fmpt 7082	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
25	22, 24	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
26	25	r19.21bi 3229	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ (𝐹‘𝑘))
27	23	fvmpt2 6979	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
28	14, 26, 27	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
29	28	an32s 652	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
30	29	mpteq2dva 5200	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ 𝐴))
31		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
32		ptcnp.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
33	32	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐼 ∈ 𝑉)
34	33	mptexd 7198	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
35		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
36	35	fvmpt2 6979	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
37	31, 34, 36	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
38	30, 37	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
39	38	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
40	39	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
41		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝐼
42		nffvmpt1 6869	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)
43	41, 42	nfmpt 5205	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
44		nffvmpt1 6869	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
45	43, 44	nfeq 2905	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
46		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
47	46	mpteq2dv 5201	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)))
48		fveq2 6858	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
49	47, 48	eqeq12d 2745	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ↔ (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
50	45, 49	rspc 3576	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
51	13, 40, 50	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
52		ptcnplem.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
53	51, 52	eqeltrd 2828	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
54	32	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ∈ 𝑉)
55		mptelixpg 8908	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
56	54, 55	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
57	53, 56	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
58	57	r19.21bi 3229	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
59		cnpimaex 23143	. . . . . . 7 ⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷) ∧ (𝐺‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
60	10, 11, 58, 59	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
61	8, 60	sylan2 593	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
62	61	ex 412	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∩ 𝑊) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))))
63	7, 62	ralrimi 3235	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
64		eleq2 2817	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (𝐷 ∈ 𝑢 ↔ 𝐷 ∈ (𝑓‘𝑘)))
65		imaeq2 6027	. . . . . 6 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) = ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)))
66	65	sseq1d 3978	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))
67	64, 66	anbi12d 632	. . . 4 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
68	67	ac6sfi 9231	. . 3 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
69	4, 63, 68	syl2anc 584	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
70	15	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
71		toponuni 22801	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
72	70, 71	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑋 = ∪ 𝐽)
73	72	ineq1d 4182	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) = (∪ 𝐽 ∩ ∩ ran 𝑓))
74		topontop 22800	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
75	15, 74	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
76	75	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ Top)
77		frn 6695	. . . . . 6 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → ran 𝑓 ⊆ 𝐽)
78	77	ad2antrl 728	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ⊆ 𝐽)
79	4	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝐼 ∩ 𝑊) ∈ Fin)
80		ffn 6688	. . . . . . . 8 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → 𝑓 Fn (𝐼 ∩ 𝑊))
81	80	ad2antrl 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓 Fn (𝐼 ∩ 𝑊))
82		dffn4 6778	. . . . . . 7 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) ↔ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
83	81, 82	sylib 218	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
84		fofi 9262	. . . . . 6 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
85	79, 83, 84	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ∈ Fin)
86		eqid 2729	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
87	86	rintopn 22796	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ∈ Fin) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
88	76, 78, 85, 87	syl3anc 1373	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
89	73, 88	eqeltrd 2828	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽)
90	12	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ 𝑋)
91		simpl 482	. . . . . . 7 ⊢ ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → 𝐷 ∈ (𝑓‘𝑘))
92	91	ralimi 3066	. . . . . 6 ⊢ (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
93	92	ad2antll 729	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
94		eleq2 2817	. . . . . . 7 ⊢ (𝑧 = (𝑓‘𝑘) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑓‘𝑘)))
95	94	ralrn 7060	. . . . . 6 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
96	81, 95	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
97	93, 96	mpbird 257	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧)
98		elrint 4953	. . . 4 ⊢ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ↔ (𝐷 ∈ 𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧))
99	90, 97, 98	sylanbrc 583	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓))
100		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑓:(𝐼 ∩ 𝑊)⟶𝐽
101	7, 100	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
102		funmpt 6554	. . . . . . . . . . . . 13 ⊢ Fun (𝑥 ∈ 𝑋 ↦ 𝐴)
103		simp-4l 782	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝜑)
104	103, 15	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
105		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
106		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ (𝐼 ∩ 𝑊))
107	105, 106	ffvelcdmd 7057	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ 𝐽)
108		toponss 22814	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓‘𝑘) ∈ 𝐽) → (𝑓‘𝑘) ⊆ 𝑋)
109	104, 107, 108	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ 𝑋)
110	106	elin1d 4167	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ 𝐼)
111	103, 110, 25	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
112		dmmptg 6215	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
113	111, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
114	109, 113	sseqtrrd 3984	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴))
115		funimass4 6925	. . . . . . . . . . . . 13 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ 𝐴) ∧ (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
116	102, 114, 115	sylancr 587	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
117		nffvmpt1 6869	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡)
118	117	nfel1 2908	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)
119		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)
120		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))
121	120	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
122	118, 119, 121	cbvralw 3280	. . . . . . . . . . . 12 ⊢ (∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))
123	116, 122	bitrdi 287	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
124		inss1 4200	. . . . . . . . . . . . 13 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋
125		ssralv 4015	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋 → (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
126	124, 111, 125	mpsyl 68	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
127		inss2 4201	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ ∩ ran 𝑓
128	105, 80	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓 Fn (𝐼 ∩ 𝑊))
129		fnfvelrn 7052	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 Fn (𝐼 ∩ 𝑊) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → (𝑓‘𝑘) ∈ ran 𝑓)
130	128, 106, 129	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ ran 𝑓)
131		intss1 4927	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑘) ∈ ran 𝑓 → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
132	130, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
133	127, 132	sstrid 3958	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘))
134		ssralv 4015	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
135	133, 134	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
136		r19.26 3091	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) ↔ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
137		elinel1 4164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → 𝑥 ∈ 𝑋)
138	137, 27	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
139	138	eleq1d 2813	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ (𝐺‘𝑘)))
140	139	biimpd 229	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → 𝐴 ∈ (𝐺‘𝑘)))
141	140	expimpd 453	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → ((𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → 𝐴 ∈ (𝐺‘𝑘)))
142	141	ralimia 3063	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
143	136, 142	sylbir 235	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
144	126, 135, 143	syl6an 684	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
145	123, 144	sylbid 240	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
146	145	expimpd 453	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
147	101, 146	ralimdaa 3238	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
148	147	impr 454	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
149		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
150		eldifi 4094	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐼 ∖ 𝑊) → 𝑘 ∈ 𝐼)
151	137, 26	sylan2 593	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → 𝐴 ∈ ∪ (𝐹‘𝑘))
152	151	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
153	149, 150, 152	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
154		ptcnplem.5	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘))
155		eleq2 2817	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (𝐴 ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ ∪ (𝐹‘𝑘)))
156	155	ralbidv 3156	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
157	154, 156	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
158	153, 157	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
159	158	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∖ 𝑊) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
160	7, 159	ralrimi 3235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
161	160	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
162		inundif 4442	. . . . . . . . 9 ⊢ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊)) = 𝐼
163	162	raleqi 3297	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
164		ralunb 4160	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
165	163, 164	bitr3i 277	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
166	148, 161, 165	sylanbrc 583	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
167		ralcom 3265	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
168	166, 167	sylibr 234	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))
169	32	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐼 ∈ 𝑉)
170		nffvmpt1 6869	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡)
171	170	nfel1 2908	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
172		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
173		fveq2 6858	. . . . . . . . 9 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
174	173	eleq1d 2813	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
175	171, 172, 174	cbvralw 3280	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
176		mptexg 7195	. . . . . . . . . . 11 ⊢ (𝐼 ∈ 𝑉 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
177	137, 176, 36	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
178	177	eleq1d 2813	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
179		mptelixpg 8908	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
180	179	adantr 480	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
181	178, 180	bitrd 279	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
182	181	ralbidva 3154	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
183	175, 182	bitrid 283	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
184	169, 183	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
185	168, 184	mpbird 257	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
186		funmpt 6554	. . . . 5 ⊢ Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
187	32	mptexd 7198	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
188	187	ralrimivw 3129	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
189	188	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
190		dmmptg 6215	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
191	189, 190	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
192	124, 191	sseqtrrid 3990	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)))
193		funimass4 6925	. . . . 5 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∧ (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
194	186, 192, 193	sylancr 587	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
195	185, 194	mpbird 257	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
196		eleq2 2817	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓)))
197		imaeq2 6027	. . . . . 6 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)))
198	197	sseq1d 3978	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
199	196, 198	anbi12d 632	. . . 4 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))))
200	199	rspcev 3588	. . 3 ⊢ (((𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
201	89, 99, 195, 200	syl12anc 836	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
202	69, 201	exlimddv 1935	1 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 Ⅎwnf 1783 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3447 ∖ cdif 3911 ∪ cun 3912 ∩ cin 3913 ⊆ wss 3914 ∪ cuni 4871 ∩ cint 4910 ↦ cmpt 5188 dom cdm 5638 ran crn 5639 “ cima 5641 Fun wfun 6505 Fn wfn 6506 ⟶wf 6507 –onto→wfo 6509 ‘cfv 6511 (class class class)co 7387 Xcixp 8870 Fincfn 8918 ∏_tcpt 17401 Topctop 22780 TopOnctopon 22797 CnP ccnp 23112

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-1o 8434 df-2o 8435 df-map 8801 df-ixp 8871 df-en 8919 df-dom 8920 df-fin 8922 df-top 22781 df-topon 22798 df-cnp 23115

This theorem is referenced by: ptcnp 23509

W3C validator