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

Theorem ptcnplem 22855
Description: Lemma for ptcnp 22856. (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 4174 . . . 4 (𝐼𝑊) ⊆ 𝑊
3 ssfi 9017 . . . 4 ((𝑊 ∈ Fin ∧ (𝐼𝑊) ⊆ 𝑊) → (𝐼𝑊) ∈ Fin)
41, 2, 3sylancl 586 . . 3 ((𝜑𝜓) → (𝐼𝑊) ∈ Fin)
5 nfv 1916 . . . . 5 𝑘𝜑
6 ptcnplem.1 . . . . 5 𝑘𝜓
75, 6nfan 1901 . . . 4 𝑘(𝜑𝜓)
8 elinel1 4140 . . . . . 6 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
9 ptcnp.7 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
109adantlr 712 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
11 ptcnplem.3 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝐺𝑘) ∈ (𝐹𝑘))
12 ptcnp.6 . . . . . . . . . . . 12 (𝜑𝐷𝑋)
1312adantr 481 . . . . . . . . . . 11 ((𝜑𝜓) → 𝐷𝑋)
14 simpr 485 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝑥𝑋)
15 ptcnp.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘𝑋))
1615adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → 𝐽 ∈ (TopOn‘𝑋))
17 ptcnp.5 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝐼⟶Top)
1817ffvelcdmda 7001 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ Top)
19 toptopon2 22150 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ Top ↔ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
2018, 19sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
21 cnpf2 22484 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷)) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2216, 20, 9, 21syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
23 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2423fmpt 7024 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑋 𝐴 (𝐹𝑘) ↔ (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2522, 24sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
2625r19.21bi 3231 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝐴 (𝐹𝑘))
2723fvmpt2 6926 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2814, 26, 27syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2928an32s 649 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3029mpteq2dva 5187 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼𝐴))
31 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → 𝑥𝑋)
32 ptcnp.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐼𝑉)
3332adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → 𝐼𝑉)
3433mptexd 7140 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ V)
35 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = (𝑥𝑋 ↦ (𝑘𝐼𝐴))
3635fvmpt2 6926 . . . . . . . . . . . . . . 15 ((𝑥𝑋 ∧ (𝑘𝐼𝐴) ∈ V) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
3731, 34, 36syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
3830, 37eqtr4d 2780 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
3938ralrimiva 3140 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
4039adantr 481 . . . . . . . . . . 11 ((𝜑𝜓) → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
41 nfcv 2905 . . . . . . . . . . . . . 14 𝑥𝐼
42 nffvmpt1 6823 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝐷)
4341, 42nfmpt 5194 . . . . . . . . . . . . 13 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷))
44 nffvmpt1 6823 . . . . . . . . . . . . 13 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
4543, 44nfeq 2918 . . . . . . . . . . . 12 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
46 fveq2 6812 . . . . . . . . . . . . . 14 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
4746mpteq2dv 5189 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)))
48 fveq2 6812 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
4947, 48eqeq12d 2753 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ↔ (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5045, 49rspc 3558 . . . . . . . . . . 11 (𝐷𝑋 → (∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5113, 40, 50sylc 65 . . . . . . . . . 10 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
52 ptcnplem.6 . . . . . . . . . 10 ((𝜑𝜓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑘𝐼 (𝐺𝑘))
5351, 52eqeltrd 2838 . . . . . . . . 9 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘))
5432adantr 481 . . . . . . . . . 10 ((𝜑𝜓) → 𝐼𝑉)
55 mptelixpg 8773 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
5654, 55syl 17 . . . . . . . . 9 ((𝜑𝜓) → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
5753, 56mpbid 231 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
5857r19.21bi 3231 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
59 cnpimaex 22490 . . . . . . 7 (((𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷) ∧ (𝐺𝑘) ∈ (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6010, 11, 58, 59syl3anc 1370 . . . . . 6 (((𝜑𝜓) ∧ 𝑘𝐼) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
618, 60sylan2 593 . . . . 5 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6261ex 413 . . . 4 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))))
637, 62ralrimi 3237 . . 3 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
64 eleq2 2826 . . . . 5 (𝑢 = (𝑓𝑘) → (𝐷𝑢𝐷 ∈ (𝑓𝑘)))
65 imaeq2 5983 . . . . . 6 (𝑢 = (𝑓𝑘) → ((𝑥𝑋𝐴) “ 𝑢) = ((𝑥𝑋𝐴) “ (𝑓𝑘)))
6665sseq1d 3962 . . . . 5 (𝑢 = (𝑓𝑘) → (((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘) ↔ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))
6764, 66anbi12d 631 . . . 4 (𝑢 = (𝑓𝑘) → ((𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)) ↔ (𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
6867ac6sfi 9131 . . 3 (((𝐼𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
694, 63, 68syl2anc 584 . 2 ((𝜑𝜓) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
7015ad2antrr 723 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
71 toponuni 22146 . . . . . 6 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7270, 71syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑋 = 𝐽)
7372ineq1d 4156 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) = ( 𝐽 ran 𝑓))
74 topontop 22145 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7515, 74syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
7675ad2antrr 723 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ Top)
77 frn 6645 . . . . . 6 (𝑓:(𝐼𝑊)⟶𝐽 → ran 𝑓𝐽)
7877ad2antrl 725 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓𝐽)
794adantr 481 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝐼𝑊) ∈ Fin)
80 ffn 6638 . . . . . . . 8 (𝑓:(𝐼𝑊)⟶𝐽𝑓 Fn (𝐼𝑊))
8180ad2antrl 725 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓 Fn (𝐼𝑊))
82 dffn4 6732 . . . . . . 7 (𝑓 Fn (𝐼𝑊) ↔ 𝑓:(𝐼𝑊)–onto→ran 𝑓)
8381, 82sylib 217 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓:(𝐼𝑊)–onto→ran 𝑓)
84 fofi 9182 . . . . . 6 (((𝐼𝑊) ∈ Fin ∧ 𝑓:(𝐼𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
8579, 83, 84syl2anc 584 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓 ∈ Fin)
86 eqid 2737 . . . . . 6 𝐽 = 𝐽
8786rintopn 22141 . . . . 5 ((𝐽 ∈ Top ∧ ran 𝑓𝐽 ∧ ran 𝑓 ∈ Fin) → ( 𝐽 ran 𝑓) ∈ 𝐽)
8876, 78, 85, 87syl3anc 1370 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ( 𝐽 ran 𝑓) ∈ 𝐽)
8973, 88eqeltrd 2838 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ∈ 𝐽)
9012ad2antrr 723 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷𝑋)
91 simpl 483 . . . . . . 7 ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → 𝐷 ∈ (𝑓𝑘))
9291ralimi 3083 . . . . . 6 (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
9392ad2antll 726 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
94 eleq2 2826 . . . . . . 7 (𝑧 = (𝑓𝑘) → (𝐷𝑧𝐷 ∈ (𝑓𝑘)))
9594ralrn 7004 . . . . . 6 (𝑓 Fn (𝐼𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
9681, 95syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
9793, 96mpbird 256 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷𝑧)
98 elrint 4935 . . . 4 (𝐷 ∈ (𝑋 ran 𝑓) ↔ (𝐷𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷𝑧))
9990, 97, 98sylanbrc 583 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷 ∈ (𝑋 ran 𝑓))
100 nfv 1916 . . . . . . . . . 10 𝑘 𝑓:(𝐼𝑊)⟶𝐽
1017, 100nfan 1901 . . . . . . . . 9 𝑘((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽)
102 funmpt 6509 . . . . . . . . . . . . 13 Fun (𝑥𝑋𝐴)
103 simp-4l 780 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝜑)
104103, 15syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
105 simpllr 773 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓:(𝐼𝑊)⟶𝐽)
106 simplr 766 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘 ∈ (𝐼𝑊))
107105, 106ffvelcdmd 7002 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ 𝐽)
108 toponss 22159 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓𝑘) ∈ 𝐽) → (𝑓𝑘) ⊆ 𝑋)
109104, 107, 108syl2anc 584 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ 𝑋)
110106elin1d 4143 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘𝐼)
111103, 110, 25syl2anc 584 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
112 dmmptg 6168 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 𝐴 (𝐹𝑘) → dom (𝑥𝑋𝐴) = 𝑋)
113111, 112syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → dom (𝑥𝑋𝐴) = 𝑋)
114109, 113sseqtrrd 3972 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴))
115 funimass4 6874 . . . . . . . . . . . . 13 ((Fun (𝑥𝑋𝐴) ∧ (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
116102, 114, 115sylancr 587 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
117 nffvmpt1 6823 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝑡)
118117nfel1 2921 . . . . . . . . . . . . 13 𝑥((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)
119 nfv 1916 . . . . . . . . . . . . 13 𝑡((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)
120 fveq2 6812 . . . . . . . . . . . . . 14 (𝑡 = 𝑥 → ((𝑥𝑋𝐴)‘𝑡) = ((𝑥𝑋𝐴)‘𝑥))
121120eleq1d 2822 . . . . . . . . . . . . 13 (𝑡 = 𝑥 → (((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
122118, 119, 121cbvralw 3286 . . . . . . . . . . . 12 (∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘))
123116, 122bitrdi 286 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
124 inss1 4173 . . . . . . . . . . . . 13 (𝑋 ran 𝑓) ⊆ 𝑋
125 ssralv 3997 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ 𝑋 → (∀𝑥𝑋 𝐴 (𝐹𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
126124, 111, 125mpsyl 68 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
127 inss2 4174 . . . . . . . . . . . . . 14 (𝑋 ran 𝑓) ⊆ ran 𝑓
128105, 80syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓 Fn (𝐼𝑊))
129 fnfvelrn 6998 . . . . . . . . . . . . . . . 16 ((𝑓 Fn (𝐼𝑊) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝑓𝑘) ∈ ran 𝑓)
130128, 106, 129syl2anc 584 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ ran 𝑓)
131 intss1 4907 . . . . . . . . . . . . . . 15 ((𝑓𝑘) ∈ ran 𝑓 ran 𝑓 ⊆ (𝑓𝑘))
132130, 131syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ran 𝑓 ⊆ (𝑓𝑘))
133127, 132sstrid 3942 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑋 ran 𝑓) ⊆ (𝑓𝑘))
134 ssralv 3997 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ (𝑓𝑘) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
135133, 134syl 17 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
136 r19.26 3111 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) ↔ (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
137 elinel1 4140 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑋 ran 𝑓) → 𝑥𝑋)
138137, 27sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
139138eleq1d 2822 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) ↔ 𝐴 ∈ (𝐺𝑘)))
140139biimpd 228 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → 𝐴 ∈ (𝐺𝑘)))
141140expimpd 454 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑋 ran 𝑓) → ((𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → 𝐴 ∈ (𝐺𝑘)))
142141ralimia 3080 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
143136, 142sylbir 234 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
144126, 135, 143syl6an 681 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
145123, 144sylbid 239 . . . . . . . . . 10 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
146145expimpd 454 . . . . . . . . 9 ((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) → ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
147101, 146ralimdaa 3240 . . . . . . . 8 (((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
148147impr 455 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
149 simpl 483 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝜑)
150 eldifi 4072 . . . . . . . . . . . 12 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
151137, 26sylan2 593 . . . . . . . . . . . . 13 (((𝜑𝑘𝐼) ∧ 𝑥 ∈ (𝑋 ran 𝑓)) → 𝐴 (𝐹𝑘))
152151ralrimiva 3140 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
153149, 150, 152syl2an 596 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
154 ptcnplem.5 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝐺𝑘) = (𝐹𝑘))
155 eleq2 2826 . . . . . . . . . . . . 13 ((𝐺𝑘) = (𝐹𝑘) → (𝐴 ∈ (𝐺𝑘) ↔ 𝐴 (𝐹𝑘)))
156155ralbidv 3171 . . . . . . . . . . . 12 ((𝐺𝑘) = (𝐹𝑘) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
157154, 156syl 17 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
158153, 157mpbird 256 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
159158ex 413 . . . . . . . . 9 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
1607, 159ralrimi 3237 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
161160adantr 481 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
162 inundif 4423 . . . . . . . . 9 ((𝐼𝑊) ∪ (𝐼𝑊)) = 𝐼
163162raleqi 3308 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
164 ralunb 4136 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
165163, 164bitr3i 276 . . . . . . 7 (∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
166148, 161, 165sylanbrc 583 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
167 ralcom 3269 . . . . . 6 (∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
168166, 167sylibr 233 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘))
16932ad2antrr 723 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐼𝑉)
170 nffvmpt1 6823 . . . . . . . . 9 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡)
171170nfel1 2921 . . . . . . . 8 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)
172 nfv 1916 . . . . . . . 8 𝑡((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)
173 fveq2 6812 . . . . . . . . 9 (𝑡 = 𝑥 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
174173eleq1d 2822 . . . . . . . 8 (𝑡 = 𝑥 → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)))
175171, 172, 174cbvralw 3286 . . . . . . 7 (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘))
176 mptexg 7137 . . . . . . . . . . 11 (𝐼𝑉 → (𝑘𝐼𝐴) ∈ V)
177137, 176, 36syl2anr 597 . . . . . . . . . 10 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
178177eleq1d 2822 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ (𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘)))
179 mptelixpg 8773 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
180179adantr 481 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
181178, 180bitrd 278 . . . . . . . 8 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
182181ralbidva 3169 . . . . . . 7 (𝐼𝑉 → (∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
183175, 182bitrid 282 . . . . . 6 (𝐼𝑉 → (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
184169, 183syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
185168, 184mpbird 256 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘))
186 funmpt 6509 . . . . 5 Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴))
18732mptexd 7140 . . . . . . . . 9 (𝜑 → (𝑘𝐼𝐴) ∈ V)
188187ralrimivw 3144 . . . . . . . 8 (𝜑 → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
189188ad2antrr 723 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
190 dmmptg 6168 . . . . . . 7 (∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
191189, 190syl 17 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
192124, 191sseqtrrid 3984 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)))
193 funimass4 6874 . . . . 5 ((Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∧ (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
194186, 192, 193sylancr 587 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
195185, 194mpbird 256 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))
196 eleq2 2826 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (𝐷𝑧𝐷 ∈ (𝑋 ran 𝑓)))
197 imaeq2 5983 . . . . . 6 (𝑧 = (𝑋 ran 𝑓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)))
198197sseq1d 3962 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘)))
199196, 198anbi12d 631 . . . 4 (𝑧 = (𝑋 ran 𝑓) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)) ↔ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))))
200199rspcev 3570 . . 3 (((𝑋 ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20189, 99, 195, 200syl12anc 834 . 2 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20269, 201exlimddv 1937 1 ((𝜑𝜓) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wex 1780  wnf 1784  wcel 2105  wral 3062  wrex 3071  Vcvv 3441  cdif 3894  cun 3895  cin 3896  wss 3897   cuni 4850   cint 4892  cmpt 5170  dom cdm 5608  ran crn 5609  cima 5611  Fun wfun 6460   Fn wfn 6461  wf 6462  ontowfo 6464  cfv 6466  (class class class)co 7317  Xcixp 8735  Fincfn 8783  tcpt 17226  Topctop 22125  TopOnctopon 22142   CnP ccnp 22459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-1st 7878  df-2nd 7879  df-1o 8346  df-er 8548  df-map 8667  df-ixp 8736  df-en 8784  df-dom 8785  df-fin 8787  df-top 22126  df-topon 22143  df-cnp 22462
This theorem is referenced by:  ptcnp  22856
  Copyright terms: Public domain W3C validator