Step | Hyp | Ref
| Expression |
1 | | frn 6607 |
. . 3
⊢ (𝐹:𝐼⟶𝒫 𝐵 → ran 𝐹 ⊆ 𝒫 𝐵) |
2 | | elrfi 40516 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ ran 𝐹 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑤))) |
3 | 1, 2 | sylan2 593 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑤))) |
4 | | imassrn 5980 |
. . . . . 6
⊢ (𝐹 “ 𝑣) ⊆ ran 𝐹 |
5 | | pwexg 5301 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → 𝒫 𝐵 ∈ V) |
6 | | ssexg 5247 |
. . . . . . . 8
⊢ ((ran
𝐹 ⊆ 𝒫 𝐵 ∧ 𝒫 𝐵 ∈ V) → ran 𝐹 ∈ V) |
7 | 1, 5, 6 | syl2anr 597 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → ran 𝐹 ∈ V) |
8 | | elpw2g 5268 |
. . . . . . 7
⊢ (ran
𝐹 ∈ V → ((𝐹 “ 𝑣) ∈ 𝒫 ran 𝐹 ↔ (𝐹 “ 𝑣) ⊆ ran 𝐹)) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → ((𝐹 “ 𝑣) ∈ 𝒫 ran 𝐹 ↔ (𝐹 “ 𝑣) ⊆ ran 𝐹)) |
10 | 4, 9 | mpbiri 257 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (𝐹 “ 𝑣) ∈ 𝒫 ran 𝐹) |
11 | 10 | adantr 481 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐹 “ 𝑣) ∈ 𝒫 ran 𝐹) |
12 | | ffun 6603 |
. . . . . 6
⊢ (𝐹:𝐼⟶𝒫 𝐵 → Fun 𝐹) |
13 | 12 | ad2antlr 724 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → Fun 𝐹) |
14 | | inss2 4163 |
. . . . . . 7
⊢
(𝒫 𝐼 ∩
Fin) ⊆ Fin |
15 | 14 | sseli 3917 |
. . . . . 6
⊢ (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣 ∈ Fin) |
16 | 15 | adantl 482 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → 𝑣 ∈ Fin) |
17 | | imafi 8958 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑣 ∈ Fin) → (𝐹 “ 𝑣) ∈ Fin) |
18 | 13, 16, 17 | syl2anc 584 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐹 “ 𝑣) ∈ Fin) |
19 | 11, 18 | elind 4128 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐹 “ 𝑣) ∈ (𝒫 ran 𝐹 ∩ Fin)) |
20 | | ffn 6600 |
. . . . . 6
⊢ (𝐹:𝐼⟶𝒫 𝐵 → 𝐹 Fn 𝐼) |
21 | 20 | ad2antlr 724 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → 𝐹 Fn 𝐼) |
22 | | inss1 4162 |
. . . . . . . 8
⊢
(𝒫 ran 𝐹
∩ Fin) ⊆ 𝒫 ran 𝐹 |
23 | 22 | sseli 3917 |
. . . . . . 7
⊢ (𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin) → 𝑤 ∈ 𝒫 ran 𝐹) |
24 | 23 | elpwid 4544 |
. . . . . 6
⊢ (𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin) → 𝑤 ⊆ ran 𝐹) |
25 | 24 | adantl 482 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → 𝑤 ⊆ ran 𝐹) |
26 | | inss2 4163 |
. . . . . . 7
⊢
(𝒫 ran 𝐹
∩ Fin) ⊆ Fin |
27 | 26 | sseli 3917 |
. . . . . 6
⊢ (𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin) → 𝑤 ∈ Fin) |
28 | 27 | adantl 482 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → 𝑤 ∈ Fin) |
29 | | fipreima 9125 |
. . . . 5
⊢ ((𝐹 Fn 𝐼 ∧ 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ∈ Fin) → ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)(𝐹 “ 𝑣) = 𝑤) |
30 | 21, 25, 28, 29 | syl3anc 1370 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)(𝐹 “ 𝑣) = 𝑤) |
31 | | eqcom 2745 |
. . . . 5
⊢ ((𝐹 “ 𝑣) = 𝑤 ↔ 𝑤 = (𝐹 “ 𝑣)) |
32 | 31 | rexbii 3181 |
. . . 4
⊢
(∃𝑣 ∈
(𝒫 𝐼 ∩
Fin)(𝐹 “ 𝑣) = 𝑤 ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝑤 = (𝐹 “ 𝑣)) |
33 | 30, 32 | sylib 217 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝑤 = (𝐹 “ 𝑣)) |
34 | | inteq 4882 |
. . . . . 6
⊢ (𝑤 = (𝐹 “ 𝑣) → ∩ 𝑤 = ∩
(𝐹 “ 𝑣)) |
35 | 34 | ineq2d 4146 |
. . . . 5
⊢ (𝑤 = (𝐹 “ 𝑣) → (𝐵 ∩ ∩ 𝑤) = (𝐵 ∩ ∩ (𝐹 “ 𝑣))) |
36 | 35 | eqeq2d 2749 |
. . . 4
⊢ (𝑤 = (𝐹 “ 𝑣) → (𝐴 = (𝐵 ∩ ∩ 𝑤) ↔ 𝐴 = (𝐵 ∩ ∩ (𝐹 “ 𝑣)))) |
37 | 36 | adantl 482 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 = (𝐹 “ 𝑣)) → (𝐴 = (𝐵 ∩ ∩ 𝑤) ↔ 𝐴 = (𝐵 ∩ ∩ (𝐹 “ 𝑣)))) |
38 | 19, 33, 37 | rexxfrd 5332 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (∃𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑤) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ (𝐹 “ 𝑣)))) |
39 | 20 | ad2antlr 724 |
. . . . . . 7
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → 𝐹 Fn 𝐼) |
40 | | inss1 4162 |
. . . . . . . . . 10
⊢
(𝒫 𝐼 ∩
Fin) ⊆ 𝒫 𝐼 |
41 | 40 | sseli 3917 |
. . . . . . . . 9
⊢ (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣 ∈ 𝒫 𝐼) |
42 | 41 | elpwid 4544 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣 ⊆ 𝐼) |
43 | 42 | adantl 482 |
. . . . . . 7
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → 𝑣 ⊆ 𝐼) |
44 | | imaiinfv 40515 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐼 ∧ 𝑣 ⊆ 𝐼) → ∩
𝑦 ∈ 𝑣 (𝐹‘𝑦) = ∩ (𝐹 “ 𝑣)) |
45 | 39, 43, 44 | syl2anc 584 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → ∩ 𝑦 ∈ 𝑣 (𝐹‘𝑦) = ∩ (𝐹 “ 𝑣)) |
46 | 45 | eqcomd 2744 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → ∩ (𝐹
“ 𝑣) = ∩ 𝑦 ∈ 𝑣 (𝐹‘𝑦)) |
47 | 46 | ineq2d 4146 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐵 ∩ ∩ (𝐹 “ 𝑣)) = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 (𝐹‘𝑦))) |
48 | 47 | eqeq2d 2749 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐴 = (𝐵 ∩ ∩ (𝐹 “ 𝑣)) ↔ 𝐴 = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 (𝐹‘𝑦)))) |
49 | 48 | rexbidva 3225 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ (𝐹 “ 𝑣)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 (𝐹‘𝑦)))) |
50 | 3, 38, 49 | 3bitrd 305 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩
𝑦 ∈ 𝑣 (𝐹‘𝑦)))) |