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

Theorem ptcnplem 21472
 Description: Lemma for ptcnp 21473. (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 3867 . . . 4 (𝐼𝑊) ⊆ 𝑊
3 ssfi 8221 . . . 4 ((𝑊 ∈ Fin ∧ (𝐼𝑊) ⊆ 𝑊) → (𝐼𝑊) ∈ Fin)
41, 2, 3sylancl 695 . . 3 ((𝜑𝜓) → (𝐼𝑊) ∈ Fin)
5 nfv 1883 . . . . 5 𝑘𝜑
6 ptcnplem.1 . . . . 5 𝑘𝜓
75, 6nfan 1868 . . . 4 𝑘(𝜑𝜓)
8 inss1 3866 . . . . . . 7 (𝐼𝑊) ⊆ 𝐼
98sseli 3632 . . . . . 6 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
10 ptcnp.7 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
1110adantlr 751 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
12 ptcnplem.3 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝐺𝑘) ∈ (𝐹𝑘))
13 ptcnp.6 . . . . . . . . . . . 12 (𝜑𝐷𝑋)
1413adantr 480 . . . . . . . . . . 11 ((𝜑𝜓) → 𝐷𝑋)
15 simpr 476 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝑥𝑋)
16 ptcnp.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘𝑋))
1716adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → 𝐽 ∈ (TopOn‘𝑋))
18 ptcnp.5 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝐼⟶Top)
1918ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ Top)
20 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑘) = (𝐹𝑘)
2120toptopon 20770 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ Top ↔ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
2219, 21sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
23 cnpf2 21102 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷)) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2417, 22, 10, 23syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
25 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2625fmpt 6421 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑋 𝐴 (𝐹𝑘) ↔ (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2724, 26sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
2827r19.21bi 2961 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝐴 (𝐹𝑘))
2925fvmpt2 6330 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3015, 28, 29syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3130an32s 863 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3231mpteq2dva 4777 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼𝐴))
33 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → 𝑥𝑋)
34 ptcnp.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐼𝑉)
3534adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → 𝐼𝑉)
36 mptexg 6525 . . . . . . . . . . . . . . . 16 (𝐼𝑉 → (𝑘𝐼𝐴) ∈ V)
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ V)
38 eqid 2651 . . . . . . . . . . . . . . . 16 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = (𝑥𝑋 ↦ (𝑘𝐼𝐴))
3938fvmpt2 6330 . . . . . . . . . . . . . . 15 ((𝑥𝑋 ∧ (𝑘𝐼𝐴) ∈ V) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
4033, 37, 39syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
4132, 40eqtr4d 2688 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
4241ralrimiva 2995 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
4342adantr 480 . . . . . . . . . . 11 ((𝜑𝜓) → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
44 nfcv 2793 . . . . . . . . . . . . . 14 𝑥𝐼
45 nffvmpt1 6237 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝐷)
4644, 45nfmpt 4779 . . . . . . . . . . . . 13 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷))
47 nffvmpt1 6237 . . . . . . . . . . . . 13 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
4846, 47nfeq 2805 . . . . . . . . . . . 12 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
49 fveq2 6229 . . . . . . . . . . . . . 14 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
5049mpteq2dv 4778 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)))
51 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
5250, 51eqeq12d 2666 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ↔ (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5348, 52rspc 3334 . . . . . . . . . . 11 (𝐷𝑋 → (∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5414, 43, 53sylc 65 . . . . . . . . . 10 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
55 ptcnplem.6 . . . . . . . . . 10 ((𝜑𝜓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑘𝐼 (𝐺𝑘))
5654, 55eqeltrd 2730 . . . . . . . . 9 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘))
5734adantr 480 . . . . . . . . . 10 ((𝜑𝜓) → 𝐼𝑉)
58 mptelixpg 7987 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
5957, 58syl 17 . . . . . . . . 9 ((𝜑𝜓) → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
6056, 59mpbid 222 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
6160r19.21bi 2961 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
62 cnpimaex 21108 . . . . . . 7 (((𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷) ∧ (𝐺𝑘) ∈ (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6311, 12, 61, 62syl3anc 1366 . . . . . 6 (((𝜑𝜓) ∧ 𝑘𝐼) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
649, 63sylan2 490 . . . . 5 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6564ex 449 . . . 4 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))))
667, 65ralrimi 2986 . . 3 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
67 eleq2 2719 . . . . 5 (𝑢 = (𝑓𝑘) → (𝐷𝑢𝐷 ∈ (𝑓𝑘)))
68 imaeq2 5497 . . . . . 6 (𝑢 = (𝑓𝑘) → ((𝑥𝑋𝐴) “ 𝑢) = ((𝑥𝑋𝐴) “ (𝑓𝑘)))
6968sseq1d 3665 . . . . 5 (𝑢 = (𝑓𝑘) → (((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘) ↔ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))
7067, 69anbi12d 747 . . . 4 (𝑢 = (𝑓𝑘) → ((𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)) ↔ (𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
7170ac6sfi 8245 . . 3 (((𝐼𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
724, 66, 71syl2anc 694 . 2 ((𝜑𝜓) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
7316ad2antrr 762 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
74 toponuni 20767 . . . . . 6 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7573, 74syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑋 = 𝐽)
7675ineq1d 3846 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) = ( 𝐽 ran 𝑓))
77 topontop 20766 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7816, 77syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
7978ad2antrr 762 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ Top)
80 frn 6091 . . . . . 6 (𝑓:(𝐼𝑊)⟶𝐽 → ran 𝑓𝐽)
8180ad2antrl 764 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓𝐽)
824adantr 480 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝐼𝑊) ∈ Fin)
83 ffn 6083 . . . . . . . 8 (𝑓:(𝐼𝑊)⟶𝐽𝑓 Fn (𝐼𝑊))
8483ad2antrl 764 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓 Fn (𝐼𝑊))
85 dffn4 6159 . . . . . . 7 (𝑓 Fn (𝐼𝑊) ↔ 𝑓:(𝐼𝑊)–onto→ran 𝑓)
8684, 85sylib 208 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓:(𝐼𝑊)–onto→ran 𝑓)
87 fofi 8293 . . . . . 6 (((𝐼𝑊) ∈ Fin ∧ 𝑓:(𝐼𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
8882, 86, 87syl2anc 694 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓 ∈ Fin)
89 eqid 2651 . . . . . 6 𝐽 = 𝐽
9089rintopn 20762 . . . . 5 ((𝐽 ∈ Top ∧ ran 𝑓𝐽 ∧ ran 𝑓 ∈ Fin) → ( 𝐽 ran 𝑓) ∈ 𝐽)
9179, 81, 88, 90syl3anc 1366 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ( 𝐽 ran 𝑓) ∈ 𝐽)
9276, 91eqeltrd 2730 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ∈ 𝐽)
9313ad2antrr 762 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷𝑋)
94 simpl 472 . . . . . . 7 ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → 𝐷 ∈ (𝑓𝑘))
9594ralimi 2981 . . . . . 6 (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
9695ad2antll 765 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
97 eleq2 2719 . . . . . . 7 (𝑧 = (𝑓𝑘) → (𝐷𝑧𝐷 ∈ (𝑓𝑘)))
9897ralrn 6402 . . . . . 6 (𝑓 Fn (𝐼𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
9984, 98syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
10096, 99mpbird 247 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷𝑧)
101 elrint 4550 . . . 4 (𝐷 ∈ (𝑋 ran 𝑓) ↔ (𝐷𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷𝑧))
10293, 100, 101sylanbrc 699 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷 ∈ (𝑋 ran 𝑓))
103 nfv 1883 . . . . . . . . . 10 𝑘 𝑓:(𝐼𝑊)⟶𝐽
1047, 103nfan 1868 . . . . . . . . 9 𝑘((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽)
105 funmpt 5964 . . . . . . . . . . . . 13 Fun (𝑥𝑋𝐴)
106 simp-4l 823 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝜑)
107106, 16syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
108 simpllr 815 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓:(𝐼𝑊)⟶𝐽)
109 simplr 807 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘 ∈ (𝐼𝑊))
110108, 109ffvelrnd 6400 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ 𝐽)
111 toponss 20779 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓𝑘) ∈ 𝐽) → (𝑓𝑘) ⊆ 𝑋)
112107, 110, 111syl2anc 694 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ 𝑋)
1138, 109sseldi 3634 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘𝐼)
114106, 113, 27syl2anc 694 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
115 dmmptg 5670 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 𝐴 (𝐹𝑘) → dom (𝑥𝑋𝐴) = 𝑋)
116114, 115syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → dom (𝑥𝑋𝐴) = 𝑋)
117112, 116sseqtr4d 3675 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴))
118 funimass4 6286 . . . . . . . . . . . . 13 ((Fun (𝑥𝑋𝐴) ∧ (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
119105, 117, 118sylancr 696 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
120 nffvmpt1 6237 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝑡)
121120nfel1 2808 . . . . . . . . . . . . 13 𝑥((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)
122 nfv 1883 . . . . . . . . . . . . 13 𝑡((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)
123 fveq2 6229 . . . . . . . . . . . . . 14 (𝑡 = 𝑥 → ((𝑥𝑋𝐴)‘𝑡) = ((𝑥𝑋𝐴)‘𝑥))
124123eleq1d 2715 . . . . . . . . . . . . 13 (𝑡 = 𝑥 → (((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
125121, 122, 124cbvral 3197 . . . . . . . . . . . 12 (∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘))
126119, 125syl6bb 276 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
127 inss1 3866 . . . . . . . . . . . . 13 (𝑋 ran 𝑓) ⊆ 𝑋
128 ssralv 3699 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ 𝑋 → (∀𝑥𝑋 𝐴 (𝐹𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
129127, 114, 128mpsyl 68 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
130 inss2 3867 . . . . . . . . . . . . . 14 (𝑋 ran 𝑓) ⊆ ran 𝑓
131108, 83syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓 Fn (𝐼𝑊))
132 fnfvelrn 6396 . . . . . . . . . . . . . . . 16 ((𝑓 Fn (𝐼𝑊) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝑓𝑘) ∈ ran 𝑓)
133131, 109, 132syl2anc 694 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ ran 𝑓)
134 intss1 4524 . . . . . . . . . . . . . . 15 ((𝑓𝑘) ∈ ran 𝑓 ran 𝑓 ⊆ (𝑓𝑘))
135133, 134syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ran 𝑓 ⊆ (𝑓𝑘))
136130, 135syl5ss 3647 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑋 ran 𝑓) ⊆ (𝑓𝑘))
137 ssralv 3699 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ (𝑓𝑘) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
138136, 137syl 17 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
139 r19.26 3093 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) ↔ (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
140127sseli 3632 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑋 ran 𝑓) → 𝑥𝑋)
141140, 29sylan 487 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
142141eleq1d 2715 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) ↔ 𝐴 ∈ (𝐺𝑘)))
143142biimpd 219 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → 𝐴 ∈ (𝐺𝑘)))
144143expimpd 628 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑋 ran 𝑓) → ((𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → 𝐴 ∈ (𝐺𝑘)))
145144ralimia 2979 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
146139, 145sylbir 225 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
147129, 138, 146syl6an 567 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
148126, 147sylbid 230 . . . . . . . . . 10 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
149148expimpd 628 . . . . . . . . 9 ((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) → ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
150104, 149ralimdaa 2987 . . . . . . . 8 (((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
151150impr 648 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
152 simpl 472 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝜑)
153 eldifi 3765 . . . . . . . . . . . 12 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
154140, 28sylan2 490 . . . . . . . . . . . . 13 (((𝜑𝑘𝐼) ∧ 𝑥 ∈ (𝑋 ran 𝑓)) → 𝐴 (𝐹𝑘))
155154ralrimiva 2995 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
156152, 153, 155syl2an 493 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
157 ptcnplem.5 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝐺𝑘) = (𝐹𝑘))
158 eleq2 2719 . . . . . . . . . . . . 13 ((𝐺𝑘) = (𝐹𝑘) → (𝐴 ∈ (𝐺𝑘) ↔ 𝐴 (𝐹𝑘)))
159158ralbidv 3015 . . . . . . . . . . . 12 ((𝐺𝑘) = (𝐹𝑘) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
160157, 159syl 17 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
161156, 160mpbird 247 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
162161ex 449 . . . . . . . . 9 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
1637, 162ralrimi 2986 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
164163adantr 480 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
165 inundif 4079 . . . . . . . . 9 ((𝐼𝑊) ∪ (𝐼𝑊)) = 𝐼
166165raleqi 3172 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
167 ralunb 3827 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
168166, 167bitr3i 266 . . . . . . 7 (∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
169151, 164, 168sylanbrc 699 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
170 ralcom 3127 . . . . . 6 (∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
171169, 170sylibr 224 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘))
17234ad2antrr 762 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐼𝑉)
173 nffvmpt1 6237 . . . . . . . . 9 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡)
174173nfel1 2808 . . . . . . . 8 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)
175 nfv 1883 . . . . . . . 8 𝑡((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)
176 fveq2 6229 . . . . . . . . 9 (𝑡 = 𝑥 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
177176eleq1d 2715 . . . . . . . 8 (𝑡 = 𝑥 → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)))
178174, 175, 177cbvral 3197 . . . . . . 7 (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘))
179140, 36, 39syl2anr 494 . . . . . . . . . 10 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
180179eleq1d 2715 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ (𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘)))
181 mptelixpg 7987 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
182181adantr 480 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
183180, 182bitrd 268 . . . . . . . 8 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
184183ralbidva 3014 . . . . . . 7 (𝐼𝑉 → (∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
185178, 184syl5bb 272 . . . . . 6 (𝐼𝑉 → (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
186172, 185syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
187171, 186mpbird 247 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘))
188 funmpt 5964 . . . . 5 Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴))
18934, 36syl 17 . . . . . . . . 9 (𝜑 → (𝑘𝐼𝐴) ∈ V)
190189ralrimivw 2996 . . . . . . . 8 (𝜑 → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
191190ad2antrr 762 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
192 dmmptg 5670 . . . . . . 7 (∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
193191, 192syl 17 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
194127, 193syl5sseqr 3687 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)))
195 funimass4 6286 . . . . 5 ((Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∧ (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
196188, 194, 195sylancr 696 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
197187, 196mpbird 247 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))
198 eleq2 2719 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (𝐷𝑧𝐷 ∈ (𝑋 ran 𝑓)))
199 imaeq2 5497 . . . . . 6 (𝑧 = (𝑋 ran 𝑓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)))
200199sseq1d 3665 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘)))
201198, 200anbi12d 747 . . . 4 (𝑧 = (𝑋 ran 𝑓) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)) ↔ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))))
202201rspcev 3340 . . 3 (((𝑋 ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20392, 102, 197, 202syl12anc 1364 . 2 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20472, 203exlimddv 1903 1 ((𝜑𝜓) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  ∃wex 1744  Ⅎwnf 1748   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∪ cuni 4468  ∩ cint 4507   ↦ cmpt 4762  dom cdm 5143  ran crn 5144   “ cima 5146  Fun wfun 5920   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  ‘cfv 5926  (class class class)co 6690  Xcixp 7950  Fincfn 7997  ∏tcpt 16146  Topctop 20746  TopOnctopon 20763   CnP ccnp 21077 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-fin 8001  df-top 20747  df-topon 20764  df-cnp 21080 This theorem is referenced by:  ptcnp  21473
 Copyright terms: Public domain W3C validator