| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elpw2g 5333 | . . . . . . 7
⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ 𝒫 𝐵 ↔ 𝐶 ⊆ 𝐵)) | 
| 2 | 1 | biimprd 248 | . . . . . 6
⊢ (𝐵 ∈ 𝑉 → (𝐶 ⊆ 𝐵 → 𝐶 ∈ 𝒫 𝐵)) | 
| 3 | 2 | ralimdv 3169 | . . . . 5
⊢ (𝐵 ∈ 𝑉 → (∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 → ∀𝑦 ∈ 𝐼 𝐶 ∈ 𝒫 𝐵)) | 
| 4 | 3 | imp 406 | . . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → ∀𝑦 ∈ 𝐼 𝐶 ∈ 𝒫 𝐵) | 
| 5 |  | eqid 2737 | . . . . 5
⊢ (𝑦 ∈ 𝐼 ↦ 𝐶) = (𝑦 ∈ 𝐼 ↦ 𝐶) | 
| 6 | 5 | fmpt 7130 | . . . 4
⊢
(∀𝑦 ∈
𝐼 𝐶 ∈ 𝒫 𝐵 ↔ (𝑦 ∈ 𝐼 ↦ 𝐶):𝐼⟶𝒫 𝐵) | 
| 7 | 4, 6 | sylib 218 | . . 3
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → (𝑦 ∈ 𝐼 ↦ 𝐶):𝐼⟶𝒫 𝐵) | 
| 8 |  | elrfirn 42706 | . . 3
⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐼 ↦ 𝐶):𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran (𝑦 ∈ 𝐼 ↦ 𝐶))) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩
𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧)))) | 
| 9 | 7, 8 | syldan 591 | . 2
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran (𝑦 ∈ 𝐼 ↦ 𝐶))) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩
𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧)))) | 
| 10 |  | inss1 4237 | . . . . . 6
⊢
(𝒫 𝐼 ∩
Fin) ⊆ 𝒫 𝐼 | 
| 11 | 10 | sseli 3979 | . . . . 5
⊢ (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣 ∈ 𝒫 𝐼) | 
| 12 | 11 | elpwid 4609 | . . . 4
⊢ (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣 ⊆ 𝐼) | 
| 13 |  | nffvmpt1 6917 | . . . . . . . 8
⊢
Ⅎ𝑦((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧) | 
| 14 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑧((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) | 
| 15 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧) = ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦)) | 
| 16 | 13, 14, 15 | cbviin 5037 | . . . . . . 7
⊢ ∩ 𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧) = ∩ 𝑦 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) | 
| 17 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼) ∧ 𝐶 ⊆ 𝐵) → 𝑦 ∈ 𝐼) | 
| 18 |  | simpll 767 | . . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼) ∧ 𝐶 ⊆ 𝐵) → 𝐵 ∈ 𝑉) | 
| 19 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼) ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ 𝐵) | 
| 20 | 18, 19 | ssexd 5324 | . . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼) ∧ 𝐶 ⊆ 𝐵) → 𝐶 ∈ V) | 
| 21 | 5 | fvmpt2 7027 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐼 ∧ 𝐶 ∈ V) → ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶) | 
| 22 | 17, 20, 21 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼) ∧ 𝐶 ⊆ 𝐵) → ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶) | 
| 23 | 22 | ex 412 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼) → (𝐶 ⊆ 𝐵 → ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶)) | 
| 24 | 23 | ralimdva 3167 | . . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → (∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 → ∀𝑦 ∈ 𝐼 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶)) | 
| 25 | 24 | imp 406 | . . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → ∀𝑦 ∈ 𝐼 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶) | 
| 26 |  | ssralv 4052 | . . . . . . . . 9
⊢ (𝑣 ⊆ 𝐼 → (∀𝑦 ∈ 𝐼 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶 → ∀𝑦 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶)) | 
| 27 | 25, 26 | mpan9 506 | . . . . . . . 8
⊢ (((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) ∧ 𝑣 ⊆ 𝐼) → ∀𝑦 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶) | 
| 28 |  | iineq2 5012 | . . . . . . . 8
⊢
(∀𝑦 ∈
𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = 𝐶 → ∩
𝑦 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = ∩ 𝑦 ∈ 𝑣 𝐶) | 
| 29 | 27, 28 | syl 17 | . . . . . . 7
⊢ (((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) ∧ 𝑣 ⊆ 𝐼) → ∩
𝑦 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑦) = ∩ 𝑦 ∈ 𝑣 𝐶) | 
| 30 | 16, 29 | eqtrid 2789 | . . . . . 6
⊢ (((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) ∧ 𝑣 ⊆ 𝐼) → ∩
𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧) = ∩ 𝑦 ∈ 𝑣 𝐶) | 
| 31 | 30 | ineq2d 4220 | . . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) ∧ 𝑣 ⊆ 𝐼) → (𝐵 ∩ ∩
𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧)) = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 𝐶)) | 
| 32 | 31 | eqeq2d 2748 | . . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) ∧ 𝑣 ⊆ 𝐼) → (𝐴 = (𝐵 ∩ ∩
𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧)) ↔ 𝐴 = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 𝐶))) | 
| 33 | 12, 32 | sylan2 593 | . . 3
⊢ (((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐴 = (𝐵 ∩ ∩
𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧)) ↔ 𝐴 = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 𝐶))) | 
| 34 | 33 | rexbidva 3177 | . 2
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → (∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩
𝑧 ∈ 𝑣 ((𝑦 ∈ 𝐼 ↦ 𝐶)‘𝑧)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 𝐶))) | 
| 35 | 9, 34 | bitrd 279 | 1
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran (𝑦 ∈ 𝐼 ↦ 𝐶))) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 𝐶))) |