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

Theorem ptcnplem 22233
 Description: Lemma for ptcnp 22234. (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.
StepHypRef Expression
1 ptcnplem.4 . . . 4 ((𝜑𝜓) → 𝑊 ∈ Fin)
2 inss2 4191 . . . 4 (𝐼𝑊) ⊆ 𝑊
3 ssfi 8735 . . . 4 ((𝑊 ∈ Fin ∧ (𝐼𝑊) ⊆ 𝑊) → (𝐼𝑊) ∈ Fin)
41, 2, 3sylancl 589 . . 3 ((𝜑𝜓) → (𝐼𝑊) ∈ Fin)
5 nfv 1916 . . . . 5 𝑘𝜑
6 ptcnplem.1 . . . . 5 𝑘𝜓
75, 6nfan 1901 . . . 4 𝑘(𝜑𝜓)
8 elinel1 4157 . . . . . 6 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
9 ptcnp.7 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
109adantlr 714 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
11 ptcnplem.3 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝐺𝑘) ∈ (𝐹𝑘))
12 ptcnp.6 . . . . . . . . . . . 12 (𝜑𝐷𝑋)
1312adantr 484 . . . . . . . . . . 11 ((𝜑𝜓) → 𝐷𝑋)
14 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝑥𝑋)
15 ptcnp.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘𝑋))
1615adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → 𝐽 ∈ (TopOn‘𝑋))
17 ptcnp.5 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝐼⟶Top)
1817ffvelrnda 6842 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ Top)
19 toptopon2 21530 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ Top ↔ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
2018, 19sylib 221 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
21 cnpf2 21862 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷)) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2216, 20, 9, 21syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
23 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2423fmpt 6865 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑋 𝐴 (𝐹𝑘) ↔ (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2522, 24sylibr 237 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
2625r19.21bi 3203 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝐴 (𝐹𝑘))
2723fvmpt2 6770 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2814, 26, 27syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2928an32s 651 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3029mpteq2dva 5147 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼𝐴))
31 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → 𝑥𝑋)
32 ptcnp.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐼𝑉)
3332adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → 𝐼𝑉)
3433mptexd 6978 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ V)
35 eqid 2824 . . . . . . . . . . . . . . . 16 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = (𝑥𝑋 ↦ (𝑘𝐼𝐴))
3635fvmpt2 6770 . . . . . . . . . . . . . . 15 ((𝑥𝑋 ∧ (𝑘𝐼𝐴) ∈ V) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
3731, 34, 36syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
3830, 37eqtr4d 2862 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
3938ralrimiva 3177 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
4039adantr 484 . . . . . . . . . . 11 ((𝜑𝜓) → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
41 nfcv 2982 . . . . . . . . . . . . . 14 𝑥𝐼
42 nffvmpt1 6672 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝐷)
4341, 42nfmpt 5149 . . . . . . . . . . . . 13 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷))
44 nffvmpt1 6672 . . . . . . . . . . . . 13 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
4543, 44nfeq 2995 . . . . . . . . . . . 12 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
46 fveq2 6661 . . . . . . . . . . . . . 14 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
4746mpteq2dv 5148 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)))
48 fveq2 6661 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
4947, 48eqeq12d 2840 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ↔ (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5045, 49rspc 3597 . . . . . . . . . . 11 (𝐷𝑋 → (∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5113, 40, 50sylc 65 . . . . . . . . . 10 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
52 ptcnplem.6 . . . . . . . . . 10 ((𝜑𝜓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑘𝐼 (𝐺𝑘))
5351, 52eqeltrd 2916 . . . . . . . . 9 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘))
5432adantr 484 . . . . . . . . . 10 ((𝜑𝜓) → 𝐼𝑉)
55 mptelixpg 8495 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
5654, 55syl 17 . . . . . . . . 9 ((𝜑𝜓) → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
5753, 56mpbid 235 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
5857r19.21bi 3203 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
59 cnpimaex 21868 . . . . . . 7 (((𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷) ∧ (𝐺𝑘) ∈ (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6010, 11, 58, 59syl3anc 1368 . . . . . 6 (((𝜑𝜓) ∧ 𝑘𝐼) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
618, 60sylan2 595 . . . . 5 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6261ex 416 . . . 4 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))))
637, 62ralrimi 3210 . . 3 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
64 eleq2 2904 . . . . 5 (𝑢 = (𝑓𝑘) → (𝐷𝑢𝐷 ∈ (𝑓𝑘)))
65 imaeq2 5912 . . . . . 6 (𝑢 = (𝑓𝑘) → ((𝑥𝑋𝐴) “ 𝑢) = ((𝑥𝑋𝐴) “ (𝑓𝑘)))
6665sseq1d 3984 . . . . 5 (𝑢 = (𝑓𝑘) → (((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘) ↔ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))
6764, 66anbi12d 633 . . . 4 (𝑢 = (𝑓𝑘) → ((𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)) ↔ (𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
6867ac6sfi 8759 . . 3 (((𝐼𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
694, 63, 68syl2anc 587 . 2 ((𝜑𝜓) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
7015ad2antrr 725 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
71 toponuni 21526 . . . . . 6 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7270, 71syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑋 = 𝐽)
7372ineq1d 4173 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) = ( 𝐽 ran 𝑓))
74 topontop 21525 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7515, 74syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
7675ad2antrr 725 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ Top)
77 frn 6509 . . . . . 6 (𝑓:(𝐼𝑊)⟶𝐽 → ran 𝑓𝐽)
7877ad2antrl 727 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓𝐽)
794adantr 484 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝐼𝑊) ∈ Fin)
80 ffn 6503 . . . . . . . 8 (𝑓:(𝐼𝑊)⟶𝐽𝑓 Fn (𝐼𝑊))
8180ad2antrl 727 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓 Fn (𝐼𝑊))
82 dffn4 6587 . . . . . . 7 (𝑓 Fn (𝐼𝑊) ↔ 𝑓:(𝐼𝑊)–onto→ran 𝑓)
8381, 82sylib 221 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓:(𝐼𝑊)–onto→ran 𝑓)
84 fofi 8807 . . . . . 6 (((𝐼𝑊) ∈ Fin ∧ 𝑓:(𝐼𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
8579, 83, 84syl2anc 587 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓 ∈ Fin)
86 eqid 2824 . . . . . 6 𝐽 = 𝐽
8786rintopn 21521 . . . . 5 ((𝐽 ∈ Top ∧ ran 𝑓𝐽 ∧ ran 𝑓 ∈ Fin) → ( 𝐽 ran 𝑓) ∈ 𝐽)
8876, 78, 85, 87syl3anc 1368 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ( 𝐽 ran 𝑓) ∈ 𝐽)
8973, 88eqeltrd 2916 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ∈ 𝐽)
9012ad2antrr 725 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷𝑋)
91 simpl 486 . . . . . . 7 ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → 𝐷 ∈ (𝑓𝑘))
9291ralimi 3155 . . . . . 6 (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
9392ad2antll 728 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
94 eleq2 2904 . . . . . . 7 (𝑧 = (𝑓𝑘) → (𝐷𝑧𝐷 ∈ (𝑓𝑘)))
9594ralrn 6845 . . . . . 6 (𝑓 Fn (𝐼𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
9681, 95syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
9793, 96mpbird 260 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷𝑧)
98 elrint 4903 . . . 4 (𝐷 ∈ (𝑋 ran 𝑓) ↔ (𝐷𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷𝑧))
9990, 97, 98sylanbrc 586 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷 ∈ (𝑋 ran 𝑓))
100 nfv 1916 . . . . . . . . . 10 𝑘 𝑓:(𝐼𝑊)⟶𝐽
1017, 100nfan 1901 . . . . . . . . 9 𝑘((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽)
102 funmpt 6381 . . . . . . . . . . . . 13 Fun (𝑥𝑋𝐴)
103 simp-4l 782 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝜑)
104103, 15syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
105 simpllr 775 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓:(𝐼𝑊)⟶𝐽)
106 simplr 768 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘 ∈ (𝐼𝑊))
107105, 106ffvelrnd 6843 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ 𝐽)
108 toponss 21539 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓𝑘) ∈ 𝐽) → (𝑓𝑘) ⊆ 𝑋)
109104, 107, 108syl2anc 587 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ 𝑋)
110106elin1d 4160 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘𝐼)
111103, 110, 25syl2anc 587 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
112 dmmptg 6083 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 𝐴 (𝐹𝑘) → dom (𝑥𝑋𝐴) = 𝑋)
113111, 112syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → dom (𝑥𝑋𝐴) = 𝑋)
114109, 113sseqtrrd 3994 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴))
115 funimass4 6721 . . . . . . . . . . . . 13 ((Fun (𝑥𝑋𝐴) ∧ (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
116102, 114, 115sylancr 590 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
117 nffvmpt1 6672 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝑡)
118117nfel1 2998 . . . . . . . . . . . . 13 𝑥((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)
119 nfv 1916 . . . . . . . . . . . . 13 𝑡((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)
120 fveq2 6661 . . . . . . . . . . . . . 14 (𝑡 = 𝑥 → ((𝑥𝑋𝐴)‘𝑡) = ((𝑥𝑋𝐴)‘𝑥))
121120eleq1d 2900 . . . . . . . . . . . . 13 (𝑡 = 𝑥 → (((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
122118, 119, 121cbvralw 3425 . . . . . . . . . . . 12 (∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘))
123116, 122syl6bb 290 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
124 inss1 4190 . . . . . . . . . . . . 13 (𝑋 ran 𝑓) ⊆ 𝑋
125 ssralv 4019 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ 𝑋 → (∀𝑥𝑋 𝐴 (𝐹𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
126124, 111, 125mpsyl 68 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
127 inss2 4191 . . . . . . . . . . . . . 14 (𝑋 ran 𝑓) ⊆ ran 𝑓
128105, 80syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓 Fn (𝐼𝑊))
129 fnfvelrn 6839 . . . . . . . . . . . . . . . 16 ((𝑓 Fn (𝐼𝑊) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝑓𝑘) ∈ ran 𝑓)
130128, 106, 129syl2anc 587 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ ran 𝑓)
131 intss1 4877 . . . . . . . . . . . . . . 15 ((𝑓𝑘) ∈ ran 𝑓 ran 𝑓 ⊆ (𝑓𝑘))
132130, 131syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ran 𝑓 ⊆ (𝑓𝑘))
133127, 132sstrid 3964 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑋 ran 𝑓) ⊆ (𝑓𝑘))
134 ssralv 4019 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ (𝑓𝑘) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
135133, 134syl 17 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
136 r19.26 3165 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) ↔ (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
137 elinel1 4157 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑋 ran 𝑓) → 𝑥𝑋)
138137, 27sylan 583 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
139138eleq1d 2900 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) ↔ 𝐴 ∈ (𝐺𝑘)))
140139biimpd 232 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → 𝐴 ∈ (𝐺𝑘)))
141140expimpd 457 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑋 ran 𝑓) → ((𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → 𝐴 ∈ (𝐺𝑘)))
142141ralimia 3153 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
143136, 142sylbir 238 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
144126, 135, 143syl6an 683 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
145123, 144sylbid 243 . . . . . . . . . 10 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
146145expimpd 457 . . . . . . . . 9 ((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) → ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
147101, 146ralimdaa 3211 . . . . . . . 8 (((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
148147impr 458 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
149 simpl 486 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝜑)
150 eldifi 4089 . . . . . . . . . . . 12 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
151137, 26sylan2 595 . . . . . . . . . . . . 13 (((𝜑𝑘𝐼) ∧ 𝑥 ∈ (𝑋 ran 𝑓)) → 𝐴 (𝐹𝑘))
152151ralrimiva 3177 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
153149, 150, 152syl2an 598 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
154 ptcnplem.5 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝐺𝑘) = (𝐹𝑘))
155 eleq2 2904 . . . . . . . . . . . . 13 ((𝐺𝑘) = (𝐹𝑘) → (𝐴 ∈ (𝐺𝑘) ↔ 𝐴 (𝐹𝑘)))
156155ralbidv 3192 . . . . . . . . . . . 12 ((𝐺𝑘) = (𝐹𝑘) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
157154, 156syl 17 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
158153, 157mpbird 260 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
159158ex 416 . . . . . . . . 9 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
1607, 159ralrimi 3210 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
161160adantr 484 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
162 inundif 4410 . . . . . . . . 9 ((𝐼𝑊) ∪ (𝐼𝑊)) = 𝐼
163162raleqi 3400 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
164 ralunb 4153 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
165163, 164bitr3i 280 . . . . . . 7 (∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
166148, 161, 165sylanbrc 586 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
167 ralcom 3345 . . . . . 6 (∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
168166, 167sylibr 237 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘))
16932ad2antrr 725 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐼𝑉)
170 nffvmpt1 6672 . . . . . . . . 9 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡)
171170nfel1 2998 . . . . . . . 8 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)
172 nfv 1916 . . . . . . . 8 𝑡((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)
173 fveq2 6661 . . . . . . . . 9 (𝑡 = 𝑥 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
174173eleq1d 2900 . . . . . . . 8 (𝑡 = 𝑥 → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)))
175171, 172, 174cbvralw 3425 . . . . . . 7 (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘))
176 mptexg 6975 . . . . . . . . . . 11 (𝐼𝑉 → (𝑘𝐼𝐴) ∈ V)
177137, 176, 36syl2anr 599 . . . . . . . . . 10 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
178177eleq1d 2900 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ (𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘)))
179 mptelixpg 8495 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
180179adantr 484 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
181178, 180bitrd 282 . . . . . . . 8 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
182181ralbidva 3191 . . . . . . 7 (𝐼𝑉 → (∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
183175, 182syl5bb 286 . . . . . 6 (𝐼𝑉 → (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
184169, 183syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
185168, 184mpbird 260 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘))
186 funmpt 6381 . . . . 5 Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴))
18732mptexd 6978 . . . . . . . . 9 (𝜑 → (𝑘𝐼𝐴) ∈ V)
188187ralrimivw 3178 . . . . . . . 8 (𝜑 → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
189188ad2antrr 725 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
190 dmmptg 6083 . . . . . . 7 (∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
191189, 190syl 17 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
192124, 191sseqtrrid 4006 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)))
193 funimass4 6721 . . . . 5 ((Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∧ (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
194186, 192, 193sylancr 590 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
195185, 194mpbird 260 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))
196 eleq2 2904 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (𝐷𝑧𝐷 ∈ (𝑋 ran 𝑓)))
197 imaeq2 5912 . . . . . 6 (𝑧 = (𝑋 ran 𝑓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)))
198197sseq1d 3984 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘)))
199196, 198anbi12d 633 . . . 4 (𝑧 = (𝑋 ran 𝑓) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)) ↔ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))))
200199rspcev 3609 . . 3 (((𝑋 ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20189, 99, 195, 200syl12anc 835 . 2 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20269, 201exlimddv 1937 1 ((𝜑𝜓) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2115  ∀wral 3133  ∃wrex 3134  Vcvv 3480   ∖ cdif 3916   ∪ cun 3917   ∩ cin 3918   ⊆ wss 3919  ∪ cuni 4824  ∩ cint 4862   ↦ cmpt 5132  dom cdm 5542  ran crn 5543   “ cima 5545  Fun wfun 6337   Fn wfn 6338  ⟶wf 6339  –onto→wfo 6341  ‘cfv 6343  (class class class)co 7149  Xcixp 8457  Fincfn 8505  ∏tcpt 16712  Topctop 21505  TopOnctopon 21522   CnP ccnp 21837 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8285  df-map 8404  df-ixp 8458  df-en 8506  df-dom 8507  df-fin 8509  df-top 21506  df-topon 21523  df-cnp 21840 This theorem is referenced by:  ptcnp  22234
 Copyright terms: Public domain W3C validator