MPE Home 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  ontowfo 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