| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ptcnplem.4 | . . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ Fin) | 
| 2 |  | inss2 4237 | . . . 4
⊢ (𝐼 ∩ 𝑊) ⊆ 𝑊 | 
| 3 |  | ssfi 9214 | . . . 4
⊢ ((𝑊 ∈ Fin ∧ (𝐼 ∩ 𝑊) ⊆ 𝑊) → (𝐼 ∩ 𝑊) ∈ Fin) | 
| 4 | 1, 2, 3 | sylancl 586 | . . 3
⊢ ((𝜑 ∧ 𝜓) → (𝐼 ∩ 𝑊) ∈ Fin) | 
| 5 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑘𝜑 | 
| 6 |  | ptcnplem.1 | . . . . 5
⊢
Ⅎ𝑘𝜓 | 
| 7 | 5, 6 | nfan 1898 | . . . 4
⊢
Ⅎ𝑘(𝜑 ∧ 𝜓) | 
| 8 |  | elinel1 4200 | . . . . . 6
⊢ (𝑘 ∈ (𝐼 ∩ 𝑊) → 𝑘 ∈ 𝐼) | 
| 9 |  | ptcnp.7 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) | 
| 10 | 9 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) | 
| 11 |  | ptcnplem.3 | . . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘)) | 
| 12 |  | ptcnp.6 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ 𝑋) | 
| 13 | 12 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ 𝑋) | 
| 14 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 15 |  | ptcnp.3 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 17 |  | ptcnp.5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹:𝐼⟶Top) | 
| 18 | 17 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ Top) | 
| 19 |  | toptopon2 22925 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑘) ∈ Top ↔ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘))) | 
| 20 | 18, 19 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘))) | 
| 21 |  | cnpf2 23259 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘)) | 
| 22 | 16, 20, 9, 21 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘)) | 
| 23 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) | 
| 24 | 23 | fmpt 7129 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘)) | 
| 25 | 22, 24 | sylibr 234 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘)) | 
| 26 | 25 | r19.21bi 3250 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ (𝐹‘𝑘)) | 
| 27 | 23 | fvmpt2 7026 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) | 
| 28 | 14, 26, 27 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) | 
| 29 | 28 | an32s 652 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) | 
| 30 | 29 | mpteq2dva 5241 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ 𝐴)) | 
| 31 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 32 |  | ptcnp.4 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐼 ∈ 𝑉) | 
| 34 | 33 | mptexd 7245 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) | 
| 35 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) | 
| 36 | 35 | fvmpt2 7026 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴)) | 
| 37 | 31, 34, 36 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴)) | 
| 38 | 30, 37 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥)) | 
| 39 | 38 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥)) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥)) | 
| 41 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝐼 | 
| 42 |  | nffvmpt1 6916 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) | 
| 43 | 41, 42 | nfmpt 5248 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) | 
| 44 |  | nffvmpt1 6916 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) | 
| 45 | 43, 44 | nfeq 2918 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) | 
| 46 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) | 
| 47 | 46 | mpteq2dv 5243 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐷 → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷))) | 
| 48 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐷 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)) | 
| 49 | 47, 48 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝐷 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ↔ (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))) | 
| 50 | 45, 49 | rspc 3609 | . . . . . . . . . . 11
⊢ (𝐷 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷))) | 
| 51 | 13, 40, 50 | sylc 65 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)) | 
| 52 |  | ptcnplem.6 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) | 
| 53 | 51, 52 | eqeltrd 2840 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) | 
| 54 | 32 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ∈ 𝑉) | 
| 55 |  | mptelixpg 8976 | . . . . . . . . . 10
⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝐼 ↦ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷)) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘))) | 
| 57 | 53, 56 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ 𝐼 ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)) | 
| 58 | 57 | r19.21bi 3250 | . . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)) | 
| 59 |  | cnpimaex 23265 | . . . . . . 7
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷) ∧ (𝐺‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝐷) ∈ (𝐺‘𝑘)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) | 
| 60 | 10, 11, 58, 59 | syl3anc 1372 | . . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) | 
| 61 | 8, 60 | sylan2 593 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) | 
| 62 | 61 | ex 412 | . . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∩ 𝑊) → ∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)))) | 
| 63 | 7, 62 | ralrimi 3256 | . . 3
⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) | 
| 64 |  | eleq2 2829 | . . . . 5
⊢ (𝑢 = (𝑓‘𝑘) → (𝐷 ∈ 𝑢 ↔ 𝐷 ∈ (𝑓‘𝑘))) | 
| 65 |  | imaeq2 6073 | . . . . . 6
⊢ (𝑢 = (𝑓‘𝑘) → ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) = ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘))) | 
| 66 | 65 | sseq1d 4014 | . . . . 5
⊢ (𝑢 = (𝑓‘𝑘) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘))) | 
| 67 | 64, 66 | anbi12d 632 | . . . 4
⊢ (𝑢 = (𝑓‘𝑘) → ((𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) | 
| 68 | 67 | ac6sfi 9321 | . . 3
⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)∃𝑢 ∈ 𝐽 (𝐷 ∈ 𝑢 ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ 𝑢) ⊆ (𝐺‘𝑘))) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) | 
| 69 | 4, 63, 68 | syl2anc 584 | . 2
⊢ ((𝜑 ∧ 𝜓) → ∃𝑓(𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) | 
| 70 | 15 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 71 |  | toponuni 22921 | . . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 72 | 70, 71 | syl 17 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑋 = ∪ 𝐽) | 
| 73 | 72 | ineq1d 4218 | . . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran
𝑓) = (∪ 𝐽
∩ ∩ ran 𝑓)) | 
| 74 |  | topontop 22920 | . . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | 
| 75 | 15, 74 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 76 | 75 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐽 ∈ Top) | 
| 77 |  | frn 6742 | . . . . . 6
⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → ran 𝑓 ⊆ 𝐽) | 
| 78 | 77 | ad2antrl 728 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ⊆ 𝐽) | 
| 79 | 4 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝐼 ∩ 𝑊) ∈ Fin) | 
| 80 |  | ffn 6735 | . . . . . . . 8
⊢ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 → 𝑓 Fn (𝐼 ∩ 𝑊)) | 
| 81 | 80 | ad2antrl 728 | . . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓 Fn (𝐼 ∩ 𝑊)) | 
| 82 |  | dffn4 6825 | . . . . . . 7
⊢ (𝑓 Fn (𝐼 ∩ 𝑊) ↔ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓) | 
| 83 | 81, 82 | sylib 218 | . . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓) | 
| 84 |  | fofi 9352 | . . . . . 6
⊢ (((𝐼 ∩ 𝑊) ∈ Fin ∧ 𝑓:(𝐼 ∩ 𝑊)–onto→ran 𝑓) → ran 𝑓 ∈ Fin) | 
| 85 | 79, 83, 84 | syl2anc 584 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ran 𝑓 ∈ Fin) | 
| 86 |  | eqid 2736 | . . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 87 | 86 | rintopn 22916 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ∈ Fin) → (∪ 𝐽
∩ ∩ ran 𝑓) ∈ 𝐽) | 
| 88 | 76, 78, 85, 87 | syl3anc 1372 | . . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∪
𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽) | 
| 89 | 73, 88 | eqeltrd 2840 | . . 3
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran
𝑓) ∈ 𝐽) | 
| 90 | 12 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ 𝑋) | 
| 91 |  | simpl 482 | . . . . . . 7
⊢ ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → 𝐷 ∈ (𝑓‘𝑘)) | 
| 92 | 91 | ralimi 3082 | . . . . . 6
⊢
(∀𝑘 ∈
(𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)) | 
| 93 | 92 | ad2antll 729 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘)) | 
| 94 |  | eleq2 2829 | . . . . . . 7
⊢ (𝑧 = (𝑓‘𝑘) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑓‘𝑘))) | 
| 95 | 94 | ralrn 7107 | . . . . . 6
⊢ (𝑓 Fn (𝐼 ∩ 𝑊) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))) | 
| 96 | 81, 95 | syl 17 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀𝑘 ∈ (𝐼 ∩ 𝑊)𝐷 ∈ (𝑓‘𝑘))) | 
| 97 | 93, 96 | mpbird 257 | . . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧) | 
| 98 |  | elrint 4988 | . . . 4
⊢ (𝐷 ∈ (𝑋 ∩ ∩ ran
𝑓) ↔ (𝐷 ∈ 𝑋 ∧ ∀𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧)) | 
| 99 | 90, 97, 98 | sylanbrc 583 | . . 3
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐷 ∈ (𝑋 ∩ ∩ ran
𝑓)) | 
| 100 |  | nfv 1913 | . . . . . . . . . 10
⊢
Ⅎ𝑘 𝑓:(𝐼 ∩ 𝑊)⟶𝐽 | 
| 101 | 7, 100 | nfan 1898 | . . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) | 
| 102 |  | funmpt 6603 | . . . . . . . . . . . . 13
⊢ Fun
(𝑥 ∈ 𝑋 ↦ 𝐴) | 
| 103 |  | simp-4l 782 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝜑) | 
| 104 | 103, 15 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 105 |  | simpllr 775 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) | 
| 106 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ (𝐼 ∩ 𝑊)) | 
| 107 | 105, 106 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ 𝐽) | 
| 108 |  | toponss 22934 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑓‘𝑘) ∈ 𝐽) → (𝑓‘𝑘) ⊆ 𝑋) | 
| 109 | 104, 107,
108 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ 𝑋) | 
| 110 | 106 | elin1d 4203 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑘 ∈ 𝐼) | 
| 111 | 103, 110,
25 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘)) | 
| 112 |  | dmmptg 6261 | . . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋) | 
| 113 | 111, 112 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → dom (𝑥 ∈ 𝑋 ↦ 𝐴) = 𝑋) | 
| 114 | 109, 113 | sseqtrrd 4020 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴)) | 
| 115 |  | funimass4 6972 | . . . . . . . . . . . . 13
⊢ ((Fun
(𝑥 ∈ 𝑋 ↦ 𝐴) ∧ (𝑓‘𝑘) ⊆ dom (𝑥 ∈ 𝑋 ↦ 𝐴)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘))) | 
| 116 | 102, 114,
115 | sylancr 587 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘))) | 
| 117 |  | nffvmpt1 6916 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) | 
| 118 | 117 | nfel1 2921 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) | 
| 119 |  | nfv 1913 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) | 
| 120 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) | 
| 121 | 120 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))) | 
| 122 | 118, 119,
121 | cbvralw 3305 | . . . . . . . . . . . 12
⊢
(∀𝑡 ∈
(𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑡) ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) | 
| 123 | 116, 122 | bitrdi 287 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))) | 
| 124 |  | inss1 4236 | . . . . . . . . . . . . 13
⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋 | 
| 125 |  | ssralv 4051 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ 𝑋 → (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))) | 
| 126 | 124, 111,
125 | mpsyl 68 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)) | 
| 127 |  | inss2 4237 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∩ ∩ ran 𝑓) ⊆ ∩ ran
𝑓 | 
| 128 | 105, 80 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → 𝑓 Fn (𝐼 ∩ 𝑊)) | 
| 129 |  | fnfvelrn 7099 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓 Fn (𝐼 ∩ 𝑊) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → (𝑓‘𝑘) ∈ ran 𝑓) | 
| 130 | 128, 106,
129 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑓‘𝑘) ∈ ran 𝑓) | 
| 131 |  | intss1 4962 | . . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑘) ∈ ran 𝑓 → ∩ ran
𝑓 ⊆ (𝑓‘𝑘)) | 
| 132 | 130, 131 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → ∩ ran
𝑓 ⊆ (𝑓‘𝑘)) | 
| 133 | 127, 132 | sstrid 3994 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (𝑋 ∩ ∩ ran
𝑓) ⊆ (𝑓‘𝑘)) | 
| 134 |  | ssralv 4051 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑘) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))) | 
| 135 | 133, 134 | syl 17 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))) | 
| 136 |  | r19.26 3110 | . . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) ↔ (∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘))) | 
| 137 |  | elinel1 4200 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓) → 𝑥 ∈ 𝑋) | 
| 138 | 137, 27 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) | 
| 139 | 138 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ (𝐺‘𝑘))) | 
| 140 | 139 | biimpd 229 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓) ∧ 𝐴 ∈ ∪ (𝐹‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → 𝐴 ∈ (𝐺‘𝑘))) | 
| 141 | 140 | expimpd 453 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓) → ((𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → 𝐴 ∈ (𝐺‘𝑘))) | 
| 142 | 141 | ralimia 3079 | . . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 143 | 136, 142 | sylbir 235 | . . . . . . . . . . . 12
⊢
((∀𝑥 ∈
(𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ ∪ (𝐹‘𝑘) ∧ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 144 | 126, 135,
143 | syl6an 684 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (∀𝑥 ∈ (𝑓‘𝑘)((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) ∈ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘))) | 
| 145 | 123, 144 | sylbid 240 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) ∧ 𝐷 ∈ (𝑓‘𝑘)) → (((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘))) | 
| 146 | 145 | expimpd 453 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) ∧ 𝑘 ∈ (𝐼 ∩ 𝑊)) → ((𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘))) | 
| 147 | 101, 146 | ralimdaa 3259 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑓:(𝐼 ∩ 𝑊)⟶𝐽) → (∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘))) | 
| 148 | 147 | impr 454 | . . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 149 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝜑) | 
| 150 |  | eldifi 4130 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐼 ∖ 𝑊) → 𝑘 ∈ 𝐼) | 
| 151 | 137, 26 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)) → 𝐴 ∈ ∪ (𝐹‘𝑘)) | 
| 152 | 151 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)) | 
| 153 | 149, 150,
152 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ ∪ (𝐹‘𝑘)) | 
| 154 |  | ptcnplem.5 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘)) | 
| 155 |  | eleq2 2829 | . . . . . . . . . . . . 13
⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (𝐴 ∈ (𝐺‘𝑘) ↔ 𝐴 ∈ ∪ (𝐹‘𝑘))) | 
| 156 | 155 | ralbidv 3177 | . . . . . . . . . . . 12
⊢ ((𝐺‘𝑘) = ∪ (𝐹‘𝑘) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))) | 
| 157 | 154, 156 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ ∪ (𝐹‘𝑘))) | 
| 158 | 153, 157 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 159 | 158 | ex 412 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ (𝐼 ∖ 𝑊) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘))) | 
| 160 | 7, 159 | ralrimi 3256 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 161 | 160 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 162 |  | inundif 4478 | . . . . . . . . 9
⊢ ((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊)) = 𝐼 | 
| 163 | 162 | raleqi 3323 | . . . . . . . 8
⊢
(∀𝑘 ∈
((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 164 |  | ralunb 4196 | . . . . . . . 8
⊢
(∀𝑘 ∈
((𝐼 ∩ 𝑊) ∪ (𝐼 ∖ 𝑊))∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘))) | 
| 165 | 163, 164 | bitr3i 277 | . . . . . . 7
⊢
(∀𝑘 ∈
𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘) ↔ (∀𝑘 ∈ (𝐼 ∩ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘) ∧ ∀𝑘 ∈ (𝐼 ∖ 𝑊)∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘))) | 
| 166 | 148, 161,
165 | sylanbrc 583 | . . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 167 |  | ralcom 3288 | . . . . . 6
⊢
(∀𝑥 ∈
(𝑋 ∩ ∩ ran 𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)𝐴 ∈ (𝐺‘𝑘)) | 
| 168 | 166, 167 | sylibr 234 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘)) | 
| 169 | 32 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → 𝐼 ∈ 𝑉) | 
| 170 |  | nffvmpt1 6916 | . . . . . . . . 9
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) | 
| 171 | 170 | nfel1 2921 | . . . . . . . 8
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) | 
| 172 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑡((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) | 
| 173 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑡 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥)) | 
| 174 | 173 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑡 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | 
| 175 | 171, 172,
174 | cbvralw 3305 | . . . . . . 7
⊢
(∀𝑡 ∈
(𝑋 ∩ ∩ ran 𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) | 
| 176 |  | mptexg 7242 | . . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑉 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) | 
| 177 | 137, 176,
36 | syl2anr 597 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) = (𝑘 ∈ 𝐼 ↦ 𝐴)) | 
| 178 | 177 | eleq1d 2825 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | 
| 179 |  | mptelixpg 8976 | . . . . . . . . . 10
⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))) | 
| 180 | 179 | adantr 480 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)) → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))) | 
| 181 | 178, 180 | bitrd 279 | . . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))) | 
| 182 | 181 | ralbidva 3175 | . . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑥) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))) | 
| 183 | 175, 182 | bitrid 283 | . . . . . 6
⊢ (𝐼 ∈ 𝑉 → (∀𝑡 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))) | 
| 184 | 169, 183 | syl 17 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (∀𝑡 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ∀𝑥 ∈ (𝑋 ∩ ∩ ran
𝑓)∀𝑘 ∈ 𝐼 𝐴 ∈ (𝐺‘𝑘))) | 
| 185 | 168, 184 | mpbird 257 | . . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑡 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) | 
| 186 |  | funmpt 6603 | . . . . 5
⊢ Fun
(𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) | 
| 187 | 32 | mptexd 7245 | . . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) | 
| 188 | 187 | ralrimivw 3149 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) | 
| 189 | 188 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∀𝑥 ∈ 𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V) | 
| 190 |  | dmmptg 6261 | . . . . . . 7
⊢
(∀𝑥 ∈
𝑋 (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ V → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋) | 
| 191 | 189, 190 | syl 17 | . . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = 𝑋) | 
| 192 | 124, 191 | sseqtrrid 4026 | . . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (𝑋 ∩ ∩ ran
𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))) | 
| 193 |  | funimass4 6972 | . . . . 5
⊢ ((Fun
(𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∧ (𝑋 ∩ ∩ ran
𝑓) ⊆ dom (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran
𝑓)) ⊆ X𝑘 ∈
𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | 
| 194 | 186, 192,
193 | sylancr 587 | . . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran
𝑓)) ⊆ X𝑘 ∈
𝐼 (𝐺‘𝑘) ↔ ∀𝑡 ∈ (𝑋 ∩ ∩ ran
𝑓)((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝑡) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | 
| 195 | 185, 194 | mpbird 257 | . . 3
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran
𝑓)) ⊆ X𝑘 ∈
𝐼 (𝐺‘𝑘)) | 
| 196 |  | eleq2 2829 | . . . . 5
⊢ (𝑧 = (𝑋 ∩ ∩ ran
𝑓) → (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran
𝑓))) | 
| 197 |  | imaeq2 6073 | . . . . . 6
⊢ (𝑧 = (𝑋 ∩ ∩ ran
𝑓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) = ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran
𝑓))) | 
| 198 | 197 | sseq1d 4014 | . . . . 5
⊢ (𝑧 = (𝑋 ∩ ∩ ran
𝑓) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran
𝑓)) ⊆ X𝑘 ∈
𝐼 (𝐺‘𝑘))) | 
| 199 | 196, 198 | anbi12d 632 | . . . 4
⊢ (𝑧 = (𝑋 ∩ ∩ ran
𝑓) → ((𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran
𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran
𝑓)) ⊆ X𝑘 ∈
𝐼 (𝐺‘𝑘)))) | 
| 200 | 199 | rspcev 3621 | . . 3
⊢ (((𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ∩ ∩ ran
𝑓) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ (𝑋 ∩ ∩ ran
𝑓)) ⊆ X𝑘 ∈
𝐼 (𝐺‘𝑘))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | 
| 201 | 89, 99, 195, 200 | syl12anc 836 | . 2
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑓:(𝐼 ∩ 𝑊)⟶𝐽 ∧ ∀𝑘 ∈ (𝐼 ∩ 𝑊)(𝐷 ∈ (𝑓‘𝑘) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴) “ (𝑓‘𝑘)) ⊆ (𝐺‘𝑘)))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | 
| 202 | 69, 201 | exlimddv 1934 | 1
⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) |