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

Theorem ptcnplem 21645
Description: Lemma for ptcnp 21646. (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 3982 . . . 4 (𝐼𝑊) ⊆ 𝑊
3 ssfi 8336 . . . 4 ((𝑊 ∈ Fin ∧ (𝐼𝑊) ⊆ 𝑊) → (𝐼𝑊) ∈ Fin)
41, 2, 3sylancl 566 . . 3 ((𝜑𝜓) → (𝐼𝑊) ∈ Fin)
5 nfv 1995 . . . . 5 𝑘𝜑
6 ptcnplem.1 . . . . 5 𝑘𝜓
75, 6nfan 1980 . . . 4 𝑘(𝜑𝜓)
8 inss1 3981 . . . . . . 7 (𝐼𝑊) ⊆ 𝐼
98sseli 3748 . . . . . 6 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
10 ptcnp.7 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
1110adantlr 686 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
12 ptcnplem.3 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → (𝐺𝑘) ∈ (𝐹𝑘))
13 ptcnp.6 . . . . . . . . . . . 12 (𝜑𝐷𝑋)
1413adantr 466 . . . . . . . . . . 11 ((𝜑𝜓) → 𝐷𝑋)
15 simpr 471 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝑥𝑋)
16 ptcnp.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘𝑋))
1716adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → 𝐽 ∈ (TopOn‘𝑋))
18 ptcnp.5 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝐼⟶Top)
1918ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ Top)
20 eqid 2771 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑘) = (𝐹𝑘)
2120toptopon 20942 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ Top ↔ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
2219, 21sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
23 cnpf2 21275 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷)) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2417, 22, 10, 23syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
25 eqid 2771 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2625fmpt 6523 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑋 𝐴 (𝐹𝑘) ↔ (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
2724, 26sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
2827r19.21bi 3081 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝐴 (𝐹𝑘))
2925fvmpt2 6433 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3015, 28, 29syl2anc 565 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3130an32s 623 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
3231mpteq2dva 4878 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼𝐴))
33 simpr 471 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → 𝑥𝑋)
34 ptcnp.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐼𝑉)
3534adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → 𝐼𝑉)
36 mptexg 6628 . . . . . . . . . . . . . . . 16 (𝐼𝑉 → (𝑘𝐼𝐴) ∈ V)
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ V)
38 eqid 2771 . . . . . . . . . . . . . . . 16 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = (𝑥𝑋 ↦ (𝑘𝐼𝐴))
3938fvmpt2 6433 . . . . . . . . . . . . . . 15 ((𝑥𝑋 ∧ (𝑘𝐼𝐴) ∈ V) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
4033, 37, 39syl2anc 565 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
4132, 40eqtr4d 2808 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
4241ralrimiva 3115 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
4342adantr 466 . . . . . . . . . . 11 ((𝜑𝜓) → ∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
44 nfcv 2913 . . . . . . . . . . . . . 14 𝑥𝐼
45 nffvmpt1 6340 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝐷)
4644, 45nfmpt 4880 . . . . . . . . . . . . 13 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷))
47 nffvmpt1 6340 . . . . . . . . . . . . 13 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
4846, 47nfeq 2925 . . . . . . . . . . . 12 𝑥(𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
49 fveq2 6332 . . . . . . . . . . . . . 14 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
5049mpteq2dv 4879 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)))
51 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
5250, 51eqeq12d 2786 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ↔ (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5348, 52rspc 3454 . . . . . . . . . . 11 (𝐷𝑋 → (∀𝑥𝑋 (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝑥)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)))
5414, 43, 53sylc 65 . . . . . . . . . 10 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷))
55 ptcnplem.6 . . . . . . . . . 10 ((𝜑𝜓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑘𝐼 (𝐺𝑘))
5654, 55eqeltrd 2850 . . . . . . . . 9 ((𝜑𝜓) → (𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘))
5734adantr 466 . . . . . . . . . 10 ((𝜑𝜓) → 𝐼𝑉)
58 mptelixpg 8099 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
5957, 58syl 17 . . . . . . . . 9 ((𝜑𝜓) → ((𝑘𝐼 ↦ ((𝑥𝑋𝐴)‘𝐷)) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)))
6056, 59mpbid 222 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘𝐼 ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
6160r19.21bi 3081 . . . . . . 7 (((𝜑𝜓) ∧ 𝑘𝐼) → ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘))
62 cnpimaex 21281 . . . . . . 7 (((𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷) ∧ (𝐺𝑘) ∈ (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝐷) ∈ (𝐺𝑘)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6311, 12, 61, 62syl3anc 1476 . . . . . 6 (((𝜑𝜓) ∧ 𝑘𝐼) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
649, 63sylan2 572 . . . . 5 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
6564ex 397 . . . 4 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))))
667, 65ralrimi 3106 . . 3 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)))
67 eleq2 2839 . . . . 5 (𝑢 = (𝑓𝑘) → (𝐷𝑢𝐷 ∈ (𝑓𝑘)))
68 imaeq2 5603 . . . . . 6 (𝑢 = (𝑓𝑘) → ((𝑥𝑋𝐴) “ 𝑢) = ((𝑥𝑋𝐴) “ (𝑓𝑘)))
6968sseq1d 3781 . . . . 5 (𝑢 = (𝑓𝑘) → (((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘) ↔ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))
7067, 69anbi12d 608 . . . 4 (𝑢 = (𝑓𝑘) → ((𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘)) ↔ (𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
7170ac6sfi 8360 . . 3 (((𝐼𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼𝑊)∃𝑢𝐽 (𝐷𝑢 ∧ ((𝑥𝑋𝐴) “ 𝑢) ⊆ (𝐺𝑘))) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
724, 66, 71syl2anc 565 . 2 ((𝜑𝜓) → ∃𝑓(𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘))))
7316ad2antrr 697 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ (TopOn‘𝑋))
74 toponuni 20939 . . . . . 6 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7573, 74syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑋 = 𝐽)
7675ineq1d 3964 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) = ( 𝐽 ran 𝑓))
77 topontop 20938 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7816, 77syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
7978ad2antrr 697 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐽 ∈ Top)
80 frn 6193 . . . . . 6 (𝑓:(𝐼𝑊)⟶𝐽 → ran 𝑓𝐽)
8180ad2antrl 699 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓𝐽)
824adantr 466 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝐼𝑊) ∈ Fin)
83 ffn 6185 . . . . . . . 8 (𝑓:(𝐼𝑊)⟶𝐽𝑓 Fn (𝐼𝑊))
8483ad2antrl 699 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓 Fn (𝐼𝑊))
85 dffn4 6262 . . . . . . 7 (𝑓 Fn (𝐼𝑊) ↔ 𝑓:(𝐼𝑊)–onto→ran 𝑓)
8684, 85sylib 208 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝑓:(𝐼𝑊)–onto→ran 𝑓)
87 fofi 8408 . . . . . 6 (((𝐼𝑊) ∈ Fin ∧ 𝑓:(𝐼𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
8882, 86, 87syl2anc 565 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ran 𝑓 ∈ Fin)
89 eqid 2771 . . . . . 6 𝐽 = 𝐽
9089rintopn 20934 . . . . 5 ((𝐽 ∈ Top ∧ ran 𝑓𝐽 ∧ ran 𝑓 ∈ Fin) → ( 𝐽 ran 𝑓) ∈ 𝐽)
9179, 81, 88, 90syl3anc 1476 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ( 𝐽 ran 𝑓) ∈ 𝐽)
9276, 91eqeltrd 2850 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ∈ 𝐽)
9313ad2antrr 697 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷𝑋)
94 simpl 468 . . . . . . 7 ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → 𝐷 ∈ (𝑓𝑘))
9594ralimi 3101 . . . . . 6 (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
9695ad2antll 700 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘))
97 eleq2 2839 . . . . . . 7 (𝑧 = (𝑓𝑘) → (𝐷𝑧𝐷 ∈ (𝑓𝑘)))
9897ralrn 6505 . . . . . 6 (𝑓 Fn (𝐼𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
9984, 98syl 17 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷𝑧 ↔ ∀𝑘 ∈ (𝐼𝑊)𝐷 ∈ (𝑓𝑘)))
10096, 99mpbird 247 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷𝑧)
101 elrint 4652 . . . 4 (𝐷 ∈ (𝑋 ran 𝑓) ↔ (𝐷𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷𝑧))
10293, 100, 101sylanbrc 564 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐷 ∈ (𝑋 ran 𝑓))
103 nfv 1995 . . . . . . . . . 10 𝑘 𝑓:(𝐼𝑊)⟶𝐽
1047, 103nfan 1980 . . . . . . . . 9 𝑘((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽)
105 funmpt 6069 . . . . . . . . . . . . 13 Fun (𝑥𝑋𝐴)
106 simp-4l 760 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝜑)
107106, 16syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝐽 ∈ (TopOn‘𝑋))
108 simpllr 752 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓:(𝐼𝑊)⟶𝐽)
109 simplr 744 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘 ∈ (𝐼𝑊))
110108, 109ffvelrnd 6503 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ 𝐽)
111 toponss 20952 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓𝑘) ∈ 𝐽) → (𝑓𝑘) ⊆ 𝑋)
112107, 110, 111syl2anc 565 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ 𝑋)
1138, 109sseldi 3750 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑘𝐼)
114106, 113, 27syl2anc 565 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
115 dmmptg 5776 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 𝐴 (𝐹𝑘) → dom (𝑥𝑋𝐴) = 𝑋)
116114, 115syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → dom (𝑥𝑋𝐴) = 𝑋)
117112, 116sseqtr4d 3791 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴))
118 funimass4 6389 . . . . . . . . . . . . 13 ((Fun (𝑥𝑋𝐴) ∧ (𝑓𝑘) ⊆ dom (𝑥𝑋𝐴)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
119105, 117, 118sylancr 567 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)))
120 nffvmpt1 6340 . . . . . . . . . . . . . 14 𝑥((𝑥𝑋𝐴)‘𝑡)
121120nfel1 2928 . . . . . . . . . . . . 13 𝑥((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘)
122 nfv 1995 . . . . . . . . . . . . 13 𝑡((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)
123 fveq2 6332 . . . . . . . . . . . . . 14 (𝑡 = 𝑥 → ((𝑥𝑋𝐴)‘𝑡) = ((𝑥𝑋𝐴)‘𝑥))
124123eleq1d 2835 . . . . . . . . . . . . 13 (𝑡 = 𝑥 → (((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
125121, 122, 124cbvral 3316 . . . . . . . . . . . 12 (∀𝑡 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑡) ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘))
126119, 125syl6bb 276 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
127 inss1 3981 . . . . . . . . . . . . 13 (𝑋 ran 𝑓) ⊆ 𝑋
128 ssralv 3815 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ 𝑋 → (∀𝑥𝑋 𝐴 (𝐹𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
129127, 114, 128mpsyl 68 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
130 inss2 3982 . . . . . . . . . . . . . 14 (𝑋 ran 𝑓) ⊆ ran 𝑓
131108, 83syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → 𝑓 Fn (𝐼𝑊))
132 fnfvelrn 6499 . . . . . . . . . . . . . . . 16 ((𝑓 Fn (𝐼𝑊) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝑓𝑘) ∈ ran 𝑓)
133131, 109, 132syl2anc 565 . . . . . . . . . . . . . . 15 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑓𝑘) ∈ ran 𝑓)
134 intss1 4626 . . . . . . . . . . . . . . 15 ((𝑓𝑘) ∈ ran 𝑓 ran 𝑓 ⊆ (𝑓𝑘))
135133, 134syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → ran 𝑓 ⊆ (𝑓𝑘))
136130, 135syl5ss 3763 . . . . . . . . . . . . 13 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (𝑋 ran 𝑓) ⊆ (𝑓𝑘))
137 ssralv 3815 . . . . . . . . . . . . 13 ((𝑋 ran 𝑓) ⊆ (𝑓𝑘) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
138136, 137syl 17 . . . . . . . . . . . 12 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
139 r19.26 3212 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) ↔ (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)))
140127sseli 3748 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑋 ran 𝑓) → 𝑥𝑋)
141140, 29sylan 561 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
142141eleq1d 2835 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) ↔ 𝐴 ∈ (𝐺𝑘)))
143142biimpd 219 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑋 ran 𝑓) ∧ 𝐴 (𝐹𝑘)) → (((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → 𝐴 ∈ (𝐺𝑘)))
144143expimpd 441 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑋 ran 𝑓) → ((𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → 𝐴 ∈ (𝐺𝑘)))
145144ralimia 3099 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋 ran 𝑓)(𝐴 (𝐹𝑘) ∧ ((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
146139, 145sylbir 225 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘) ∧ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
147129, 138, 146syl6an 655 . . . . . . . . . . 11 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (∀𝑥 ∈ (𝑓𝑘)((𝑥𝑋𝐴)‘𝑥) ∈ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
148126, 147sylbid 230 . . . . . . . . . 10 (((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) ∧ 𝐷 ∈ (𝑓𝑘)) → (((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
149148expimpd 441 . . . . . . . . 9 ((((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼𝑊)) → ((𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
150104, 149ralimdaa 3107 . . . . . . . 8 (((𝜑𝜓) ∧ 𝑓:(𝐼𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
151150impr 442 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
152 simpl 468 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝜑)
153 eldifi 3883 . . . . . . . . . . . 12 (𝑘 ∈ (𝐼𝑊) → 𝑘𝐼)
154140, 28sylan2 572 . . . . . . . . . . . . 13 (((𝜑𝑘𝐼) ∧ 𝑥 ∈ (𝑋 ran 𝑓)) → 𝐴 (𝐹𝑘))
155154ralrimiva 3115 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
156152, 153, 155syl2an 575 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘))
157 ptcnplem.5 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (𝐺𝑘) = (𝐹𝑘))
158 eleq2 2839 . . . . . . . . . . . . 13 ((𝐺𝑘) = (𝐹𝑘) → (𝐴 ∈ (𝐺𝑘) ↔ 𝐴 (𝐹𝑘)))
159158ralbidv 3135 . . . . . . . . . . . 12 ((𝐺𝑘) = (𝐹𝑘) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
160157, 159syl 17 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → (∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 (𝐹𝑘)))
161156, 160mpbird 247 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑘 ∈ (𝐼𝑊)) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
162161ex 397 . . . . . . . . 9 ((𝜑𝜓) → (𝑘 ∈ (𝐼𝑊) → ∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
1637, 162ralrimi 3106 . . . . . . . 8 ((𝜑𝜓) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
164163adantr 466 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
165 inundif 4188 . . . . . . . . 9 ((𝐼𝑊) ∪ (𝐼𝑊)) = 𝐼
166165raleqi 3291 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
167 ralunb 3945 . . . . . . . 8 (∀𝑘 ∈ ((𝐼𝑊) ∪ (𝐼𝑊))∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
168166, 167bitr3i 266 . . . . . . 7 (∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ↔ (∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘) ∧ ∀𝑘 ∈ (𝐼𝑊)∀𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘)))
169151, 164, 168sylanbrc 564 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
170 ralcom 3246 . . . . . 6 (∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘) ↔ ∀𝑘𝐼𝑥 ∈ (𝑋 ran 𝑓)𝐴 ∈ (𝐺𝑘))
171169, 170sylibr 224 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥 ∈ (𝑋 ran 𝑓)∀𝑘𝐼 𝐴 ∈ (𝐺𝑘))
17234ad2antrr 697 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → 𝐼𝑉)
173 nffvmpt1 6340 . . . . . . . . 9 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡)
174173nfel1 2928 . . . . . . . 8 𝑥((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)
175 nfv 1995 . . . . . . . 8 𝑡((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)
176 fveq2 6332 . . . . . . . . 9 (𝑡 = 𝑥 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥))
177176eleq1d 2835 . . . . . . . 8 (𝑡 = 𝑥 → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘)))
178174, 175, 177cbvral 3316 . . . . . . 7 (∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑥 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘))
179140, 36, 39syl2anr 576 . . . . . . . . . 10 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) = (𝑘𝐼𝐴))
180179eleq1d 2835 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ (𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘)))
181 mptelixpg 8099 . . . . . . . . . 10 (𝐼𝑉 → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
182181adantr 466 . . . . . . . . 9 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
183180, 182bitrd 268 . . . . . . . 8 ((𝐼𝑉𝑥 ∈ (𝑋 ran 𝑓)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑥) ∈ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑘𝐼 𝐴 ∈ (𝐺𝑘)))
184183ralbidva 3134 . . . . . . 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 6069 . . . . 5 Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴))
18934, 36syl 17 . . . . . . . . 9 (𝜑 → (𝑘𝐼𝐴) ∈ V)
190189ralrimivw 3116 . . . . . . . 8 (𝜑 → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
191190ad2antrr 697 . . . . . . 7 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V)
192 dmmptg 5776 . . . . . . 7 (∀𝑥𝑋 (𝑘𝐼𝐴) ∈ V → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
193191, 192syl 17 . . . . . 6 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = 𝑋)
194127, 193syl5sseqr 3803 . . . . 5 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴)))
195 funimass4 6389 . . . . 5 ((Fun (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∧ (𝑋 ran 𝑓) ⊆ dom (𝑥𝑋 ↦ (𝑘𝐼𝐴))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
196188, 194, 195sylancr 567 . . . 4 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ∀𝑡 ∈ (𝑋 ran 𝑓)((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝑡) ∈ X𝑘𝐼 (𝐺𝑘)))
197187, 196mpbird 247 . . 3 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))
198 eleq2 2839 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (𝐷𝑧𝐷 ∈ (𝑋 ran 𝑓)))
199 imaeq2 5603 . . . . . 6 (𝑧 = (𝑋 ran 𝑓) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) = ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)))
200199sseq1d 3781 . . . . 5 (𝑧 = (𝑋 ran 𝑓) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘)))
201198, 200anbi12d 608 . . . 4 (𝑧 = (𝑋 ran 𝑓) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)) ↔ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))))
202201rspcev 3460 . . 3 (((𝑋 ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ran 𝑓) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ (𝑋 ran 𝑓)) ⊆ X𝑘𝐼 (𝐺𝑘))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20392, 102, 197, 202syl12anc 1474 . 2 (((𝜑𝜓) ∧ (𝑓:(𝐼𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼𝑊)(𝐷 ∈ (𝑓𝑘) ∧ ((𝑥𝑋𝐴) “ (𝑓𝑘)) ⊆ (𝐺𝑘)))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
20472, 203exlimddv 2015 1 ((𝜑𝜓) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝐺𝑘)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wex 1852  wnf 1856  wcel 2145  wral 3061  wrex 3062  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723   cuni 4574   cint 4611  cmpt 4863  dom cdm 5249  ran crn 5250  cima 5252  Fun wfun 6025   Fn wfn 6026  wf 6027  ontowfo 6029  cfv 6031  (class class class)co 6793  Xcixp 8062  Fincfn 8109  tcpt 16307  Topctop 20918  TopOnctopon 20935   CnP ccnp 21250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-ixp 8063  df-en 8110  df-dom 8111  df-fin 8113  df-top 20919  df-topon 20936  df-cnp 21253
This theorem is referenced by:  ptcnp  21646
  Copyright terms: Public domain W3C validator