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 22772

Description: Lemma for ptcnp 22773. (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 4163	. . . 4 ⊢ (𝐼 ∩ 𝑊) ⊆ 𝑊
3		ssfi 8956	. . . 4 ⊢ ((𝑊 ∈ Fin ∧ (𝐼 ∩ 𝑊) ⊆ 𝑊) → (𝐼 ∩ 𝑊) ∈ Fin)
4	1, 2, 3	sylancl 586	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝐼 ∩ 𝑊) ∈ Fin)
5		nfv 1917	. . . . 5 ⊢ Ⅎ𝑘𝜑
6		ptcnplem.1	. . . . 5 ⊢ Ⅎ𝑘𝜓
7	5, 6	nfan 1902	. . . 4 ⊢ Ⅎ𝑘(𝜑 ∧ 𝜓)
8		elinel1 4129	. . . . . 6 ⊢ (𝑘 ∈ (𝐼 ∩ 𝑊) → 𝑘 ∈ 𝐼)
9		ptcnp.7	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
10	9	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
11		ptcnplem.3	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘))
12		ptcnp.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
13	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ 𝑋)
14		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
15		ptcnp.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
16	15	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐽 ∈ (TopOn‘𝑋))
17		ptcnp.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:𝐼⟶Top)
18	17	ffvelrnda 6961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ Top)
19		toptopon2 22067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ Top ↔ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
20	18, 19	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
21		cnpf2 22401	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
22	16, 20, 9, 21	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
23		eqid 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴)
24	23	fmpt 6984	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
25	22, 24	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
26	25	r19.21bi 3134	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ (𝐹‘𝑘))
27	23	fvmpt2 6886	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
28	14, 26, 27	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
29	28	an32s 649	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
30	29	mpteq2dva 5174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ 𝐴))
31		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
32		ptcnp.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
33	32	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐼 ∈ 𝑉)
34	33	mptexd 7100	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
35		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
36	35	fvmpt2 6886	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
37	31, 34, 36	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
38	30, 37	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
39	38	ralrimiva 3103	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
40	39	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
41		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝐼
42		nffvmpt1 6785	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)
43	41, 42	nfmpt 5181	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
44		nffvmpt1 6785	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
45	43, 44	nfeq 2920	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
46		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))
47	46	mpteq2dv 5176	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)))
48		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
49	47, 48	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ↔ (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
50	45, 49	rspc 3549	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)))
51	13, 40, 50	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))
52		ptcnplem.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
53	51, 52	eqeltrd 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
54	32	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ∈ 𝑉)
55		mptelixpg 8723	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
56	54, 55	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)))
57	53, 56	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
58	57	r19.21bi 3134	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))
59		cnpimaex 22407	. . . . . . 7 ⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷) ∧ (𝐺‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
60	10, 11, 58, 59	syl3anc 1370	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
61	8, 60	sylan2 593	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
62	61	ex 413	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∩ 𝑊) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))))
63	7, 62	ralrimi 3141	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))
64		eleq2 2827	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (𝐷 ∈ 𝑢 ↔ 𝐷 ∈ (𝑓‘𝑘)))
65		imaeq2 5965	. . . . . 6 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) = ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)))
66	65	sseq1d 3952	. . . . 5 ⊢ (𝑢 = (𝑓‘𝑘) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))
67	64, 66	anbi12d 631	. . . 4 ⊢ (𝑢 = (𝑓‘𝑘) → ((𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
68	67	ac6sfi 9058	. . 3 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
69	4, 63, 68	syl2anc 584	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))))
70	15	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
71		toponuni 22063	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
72	70, 71	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑋 = ∪ 𝐽)
73	72	ineq1d 4145	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) = (∪ 𝐽 ∩ ∩ ran 𝑓))
74		topontop 22062	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
75	15, 74	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
76	75	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ Top)
77		frn 6607	. . . . . 6 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → ran 𝑓 ⊆ 𝐽)
78	77	ad2antrl 725	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ⊆ 𝐽)
79	4	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝐼 ∩ 𝑊) ∈ Fin)
80		ffn 6600	. . . . . . . 8 ⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → 𝑓 Fn (𝐼 ∩ 𝑊))
81	80	ad2antrl 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓 Fn (𝐼 ∩ 𝑊))
82		dffn4 6694	. . . . . . 7 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) ↔ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
83	81, 82	sylib 217	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓)
84		fofi 9105	. . . . . 6 ⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
85	79, 83, 84	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ∈ Fin)
86		eqid 2738	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
87	86	rintopn 22058	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ∈ Fin) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
88	76, 78, 85, 87	syl3anc 1370	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∪ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
89	73, 88	eqeltrd 2839	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽)
90	12	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ 𝑋)
91		simpl 483	. . . . . . 7 ⊢ ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → 𝐷 ∈ (𝑓‘𝑘))
92	91	ralimi 3087	. . . . . 6 ⊢ (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
93	92	ad2antll 726	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))
94		eleq2 2827	. . . . . . 7 ⊢ (𝑧 = (𝑓‘𝑘) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑓‘𝑘)))
95	94	ralrn 6964	. . . . . 6 ⊢ (𝑓 Fn (𝐼 ∩ 𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
96	81, 95	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)))
97	93, 96	mpbird 256	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧)
98		elrint 4922	. . . 4 ⊢ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ↔ (𝐷 ∈ 𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧))
99	90, 97, 98	sylanbrc 583	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓))
100		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑓:(𝐼 ∩ 𝑊)⟶𝐽
101	7, 100	nfan 1902	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
102		funmpt 6472	. . . . . . . . . . . . 13 ⊢ Fun (𝑥 ∈ 𝑋 ↦ 𝐴)
103		simp-4l 780	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝜑)
104	103, 15	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
105		simpllr 773	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓:(𝐼 ∩ 𝑊)⟶𝐽)
106		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ (𝐼 ∩ 𝑊))
107	105, 106	ffvelrnd 6962	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ 𝐽)
108		toponss 22076	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓‘𝑘) ∈ 𝐽) → (𝑓‘𝑘) ⊆ 𝑋)
109	104, 107, 108	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ 𝑋)
110	106	elin1d 4132	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ 𝐼)
111	103, 110, 25	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
112		dmmptg 6145	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
113	111, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋)
114	109, 113	sseqtrrd 3962	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴))
115		funimass4 6834	. . . . . . . . . . . . 13 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ 𝐴) ∧ (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
116	102, 114, 115	sylancr 587	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)))
117		nffvmpt1 6785	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡)
118	117	nfel1 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘)
119		nfv 1917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)
120		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))
121	120	eleq1d 2823	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
122	118, 119, 121	cbvralw 3373	. . . . . . . . . . . 12 ⊢ (∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))
123	116, 122	bitrdi 287	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
124		inss1 4162	. . . . . . . . . . . . 13 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋
125		ssralv 3987	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋 → (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
126	124, 111, 125	mpsyl 68	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
127		inss2 4163	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ ∩ ran 𝑓
128	105, 80	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓 Fn (𝐼 ∩ 𝑊))
129		fnfvelrn 6958	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 Fn (𝐼 ∩ 𝑊) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → (𝑓‘𝑘) ∈ ran 𝑓)
130	128, 106, 129	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ ran 𝑓)
131		intss1 4894	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑘) ∈ ran 𝑓 → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
132	130, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∩ ran 𝑓 ⊆ (𝑓‘𝑘))
133	127, 132	sstrid 3932	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘))
134		ssralv 3987	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
135	133, 134	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
136		r19.26 3095	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) ↔ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)))
137		elinel1 4129	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → 𝑥 ∈ 𝑋)
138	137, 27	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴)
139	138	eleq1d 2823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ (𝐺‘𝑘)))
140	139	biimpd 228	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → 𝐴 ∈ (𝐺‘𝑘)))
141	140	expimpd 454	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓) → ((𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → 𝐴 ∈ (𝐺‘𝑘)))
142	141	ralimia 3085	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
143	136, 142	sylbir 234	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
144	126, 135, 143	syl6an 681	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
145	123, 144	sylbid 239	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
146	145	expimpd 454	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
147	101, 146	ralimdaa 3142	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
148	147	impr 455	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
149		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
150		eldifi 4061	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐼 ∖ 𝑊) → 𝑘 ∈ 𝐼)
151	137, 26	sylan2 593	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → 𝐴 ∈ ∪ (𝐹‘𝑘))
152	151	ralrimiva 3103	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
153	149, 150, 152	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))
154		ptcnplem.5	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘))
155		eleq2 2827	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (𝐴 ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ ∪ (𝐹‘𝑘)))
156	155	ralbidv 3112	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
157	154, 156	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)))
158	153, 157	mpbird 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
159	158	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∖ 𝑊) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
160	7, 159	ralrimi 3141	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
161	160	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
162		inundif 4412	. . . . . . . . 9 ⊢ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊)) = 𝐼
163	162	raleqi 3346	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
164		ralunb 4125	. . . . . . . 8 ⊢ (∀𝑘 ∈ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
165	163, 164	bitr3i 276	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘)))
166	148, 161, 165	sylanbrc 583	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
167		ralcom 3166	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (𝐺‘𝑘))
168	166, 167	sylibr 233	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))
169	32	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐼 ∈ 𝑉)
170		nffvmpt1 6785	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡)
171	170	nfel1 2923	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
172		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)
173		fveq2 6774	. . . . . . . . 9 ⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥))
174	173	eleq1d 2823	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
175	171, 172, 174	cbvralw 3373	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
176		mptexg 7097	. . . . . . . . . . 11 ⊢ (𝐼 ∈ 𝑉 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
177	137, 176, 36	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴))
178	177	eleq1d 2823	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
179		mptelixpg 8723	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
180	179	adantr 481	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
181	178, 180	bitrd 278	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
182	181	ralbidva 3111	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
183	175, 182	bitrid 282	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
184	169, 183	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)))
185	168, 184	mpbird 256	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
186		funmpt 6472	. . . . 5 ⊢ Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
187	32	mptexd 7100	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
188	187	ralrimivw 3104	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
189	188	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V)
190		dmmptg 6145	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
191	189, 190	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋)
192	124, 191	sseqtrrid 3974	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)))
193		funimass4 6834	. . . . 5 ⊢ ((Fun (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∧ (𝑋 ∩ ∩ ran 𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
194	186, 192, 193	sylancr 587	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
195	185, 194	mpbird 256	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))
196		eleq2 2827	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓)))
197		imaeq2 5965	. . . . . 6 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)))
198	197	sseq1d 3952	. . . . 5 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
199	196, 198	anbi12d 631	. . . 4 ⊢ (𝑧 = (𝑋 ∩ ∩ ran 𝑓) → ((𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))))
200	199	rspcev 3561	. . 3 ⊢ (((𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran 𝑓)) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
201	89, 99, 195, 200	syl12anc 834	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
202	69, 201	exlimddv 1938	1 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 Vcvv 3432 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∪ cuni 4839 ∩ cint 4879 ↦ cmpt 5157 dom cdm 5589 ran crn 5590 “ cima 5592 Fun wfun 6427 Fn wfn 6428 ⟶wf 6429 –onto→wfo 6431 ‘cfv 6433 (class class class)co 7275 Xcixp 8685 Fincfn 8733 ∏_tcpt 17149 Topctop 22042 TopOnctopon 22059 CnP ccnp 22376

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-1o 8297 df-er 8498 df-map 8617 df-ixp 8686 df-en 8734 df-dom 8735 df-fin 8737 df-top 22043 df-topon 22060 df-cnp 22379

This theorem is referenced by: ptcnp 22773

W3C validator