Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. . 3
⊢ (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) → 𝐴 ∈ V) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) → 𝐴 ∈ V)) |
3 | | inex1g 4729 |
. . . . 5
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∩ ∩ 𝑣) ∈ V) |
4 | | eleq1 2676 |
. . . . 5
⊢ (𝐴 = (𝐵 ∩ ∩ 𝑣) → (𝐴 ∈ V ↔ (𝐵 ∩ ∩ 𝑣) ∈ V)) |
5 | 3, 4 | syl5ibrcom 236 |
. . . 4
⊢ (𝐵 ∈ 𝑉 → (𝐴 = (𝐵 ∩ ∩ 𝑣) → 𝐴 ∈ V)) |
6 | 5 | rexlimdvw 3016 |
. . 3
⊢ (𝐵 ∈ 𝑉 → (∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣) → 𝐴 ∈ V)) |
7 | 6 | adantr 480 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣) → 𝐴 ∈ V)) |
8 | | simpr 476 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → 𝐴 ∈ V) |
9 | | snex 4835 |
. . . . . 6
⊢ {𝐵} ∈ V |
10 | | pwexg 4776 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → 𝒫 𝐵 ∈ V) |
11 | 10 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → 𝒫 𝐵 ∈ V) |
12 | | simplr 788 |
. . . . . . 7
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → 𝐶 ⊆ 𝒫 𝐵) |
13 | 11, 12 | ssexd 4733 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → 𝐶 ∈ V) |
14 | | unexg 6857 |
. . . . . 6
⊢ (({𝐵} ∈ V ∧ 𝐶 ∈ V) → ({𝐵} ∪ 𝐶) ∈ V) |
15 | 9, 13, 14 | sylancr 694 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → ({𝐵} ∪ 𝐶) ∈ V) |
16 | | elfi 8202 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ({𝐵} ∪ 𝐶) ∈ V) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)𝐴 = ∩ 𝑤)) |
17 | 8, 15, 16 | syl2anc 691 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)𝐴 = ∩ 𝑤)) |
18 | | inss1 3795 |
. . . . . . . . . . . 12
⊢
(𝒫 ({𝐵}
∪ 𝐶) ∩ Fin) ⊆
𝒫 ({𝐵} ∪ 𝐶) |
19 | | uncom 3719 |
. . . . . . . . . . . . 13
⊢ ({𝐵} ∪ 𝐶) = (𝐶 ∪ {𝐵}) |
20 | 19 | pweqi 4112 |
. . . . . . . . . . . 12
⊢ 𝒫
({𝐵} ∪ 𝐶) = 𝒫 (𝐶 ∪ {𝐵}) |
21 | 18, 20 | sseqtri 3600 |
. . . . . . . . . . 11
⊢
(𝒫 ({𝐵}
∪ 𝐶) ∩ Fin) ⊆
𝒫 (𝐶 ∪ {𝐵}) |
22 | 21 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) → 𝑤 ∈ 𝒫 (𝐶 ∪ {𝐵})) |
23 | 9 | elpwun 6869 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝒫 (𝐶 ∪ {𝐵}) ↔ (𝑤 ∖ {𝐵}) ∈ 𝒫 𝐶) |
24 | 22, 23 | sylib 207 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) → (𝑤 ∖ {𝐵}) ∈ 𝒫 𝐶) |
25 | 24 | ad2antrl 760 |
. . . . . . . 8
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → (𝑤 ∖ {𝐵}) ∈ 𝒫 𝐶) |
26 | | inss2 3796 |
. . . . . . . . . . 11
⊢
(𝒫 ({𝐵}
∪ 𝐶) ∩ Fin) ⊆
Fin |
27 | 26 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) → 𝑤 ∈ Fin) |
28 | | diffi 8077 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Fin → (𝑤 ∖ {𝐵}) ∈ Fin) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) → (𝑤 ∖ {𝐵}) ∈ Fin) |
30 | 29 | ad2antrl 760 |
. . . . . . . 8
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → (𝑤 ∖ {𝐵}) ∈ Fin) |
31 | 25, 30 | elind 3760 |
. . . . . . 7
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → (𝑤 ∖ {𝐵}) ∈ (𝒫 𝐶 ∩ Fin)) |
32 | | incom 3767 |
. . . . . . . . . . . 12
⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) |
33 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 = ∩ 𝑤) |
34 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 ∈ V) |
35 | 33, 34 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → ∩ 𝑤
∈ V) |
36 | | intex 4747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ≠ ∅ ↔ ∩ 𝑤
∈ V) |
37 | 35, 36 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝑤 ≠ ∅) |
38 | | intssuni 4434 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ≠ ∅ → ∩ 𝑤
⊆ ∪ 𝑤) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → ∩ 𝑤
⊆ ∪ 𝑤) |
40 | 18 | sseli 3564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) → 𝑤 ∈ 𝒫 ({𝐵} ∪ 𝐶)) |
41 | 40 | elpwid 4118 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) → 𝑤 ⊆ ({𝐵} ∪ 𝐶)) |
42 | 41 | ad2antrl 760 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝑤 ⊆ ({𝐵} ∪ 𝐶)) |
43 | | pwidg 4121 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵) |
44 | 43 | snssd 4281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ 𝑉 → {𝐵} ⊆ 𝒫 𝐵) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → {𝐵} ⊆ 𝒫 𝐵) |
46 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → 𝐶 ⊆ 𝒫 𝐵) |
47 | 45, 46 | unssd 3751 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → ({𝐵} ∪ 𝐶) ⊆ 𝒫 𝐵) |
48 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → ({𝐵} ∪ 𝐶) ⊆ 𝒫 𝐵) |
49 | 42, 48 | sstrd 3578 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝑤 ⊆ 𝒫 𝐵) |
50 | | sspwuni 4547 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ⊆ 𝒫 𝐵 ↔ ∪ 𝑤
⊆ 𝐵) |
51 | 49, 50 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → ∪ 𝑤
⊆ 𝐵) |
52 | 39, 51 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → ∩ 𝑤
⊆ 𝐵) |
53 | 33, 52 | eqsstrd 3602 |
. . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 ⊆ 𝐵) |
54 | | df-ss 3554 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
55 | 53, 54 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → (𝐴 ∩ 𝐵) = 𝐴) |
56 | 32, 55 | syl5req 2657 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 = (𝐵 ∩ 𝐴)) |
57 | | ineq2 3770 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∩
𝑤 → (𝐵 ∩ 𝐴) = (𝐵 ∩ ∩ 𝑤)) |
58 | 57 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → (𝐵 ∩ 𝐴) = (𝐵 ∩ ∩ 𝑤)) |
59 | 56, 58 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 = (𝐵 ∩ ∩ 𝑤)) |
60 | | intun 4444 |
. . . . . . . . . . . 12
⊢ ∩ ({𝐵}
∪ 𝑤) = (∩ {𝐵}
∩ ∩ 𝑤) |
61 | | intsng 4447 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ 𝑉 → ∩ {𝐵} = 𝐵) |
62 | 61 | ineq1d 3775 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑉 → (∩ {𝐵} ∩ ∩ 𝑤) =
(𝐵 ∩ ∩ 𝑤)) |
63 | 60, 62 | syl5req 2657 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∩ ∩ 𝑤) = ∩
({𝐵} ∪ 𝑤)) |
64 | 63 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → (𝐵 ∩ ∩ 𝑤) = ∩
({𝐵} ∪ 𝑤)) |
65 | 59, 64 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 = ∩ ({𝐵} ∪ 𝑤)) |
66 | | undif2 3996 |
. . . . . . . . . 10
⊢ ({𝐵} ∪ (𝑤 ∖ {𝐵})) = ({𝐵} ∪ 𝑤) |
67 | 66 | inteqi 4414 |
. . . . . . . . 9
⊢ ∩ ({𝐵}
∪ (𝑤 ∖ {𝐵})) = ∩ ({𝐵}
∪ 𝑤) |
68 | 65, 67 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 = ∩ ({𝐵} ∪ (𝑤 ∖ {𝐵}))) |
69 | | intun 4444 |
. . . . . . . . . 10
⊢ ∩ ({𝐵}
∪ (𝑤 ∖ {𝐵})) = (∩ {𝐵}
∩ ∩ (𝑤 ∖ {𝐵})) |
70 | 61 | ineq1d 3775 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → (∩ {𝐵} ∩ ∩ (𝑤
∖ {𝐵})) = (𝐵 ∩ ∩ (𝑤
∖ {𝐵}))) |
71 | 69, 70 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → ∩ ({𝐵} ∪ (𝑤 ∖ {𝐵})) = (𝐵 ∩ ∩ (𝑤 ∖ {𝐵}))) |
72 | 71 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → ∩ ({𝐵}
∪ (𝑤 ∖ {𝐵})) = (𝐵 ∩ ∩ (𝑤 ∖ {𝐵}))) |
73 | 68, 72 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → 𝐴 = (𝐵 ∩ ∩ (𝑤 ∖ {𝐵}))) |
74 | | inteq 4413 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑤 ∖ {𝐵}) → ∩ 𝑣 = ∩
(𝑤 ∖ {𝐵})) |
75 | 74 | ineq2d 3776 |
. . . . . . . . 9
⊢ (𝑣 = (𝑤 ∖ {𝐵}) → (𝐵 ∩ ∩ 𝑣) = (𝐵 ∩ ∩ (𝑤 ∖ {𝐵}))) |
76 | 75 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑣 = (𝑤 ∖ {𝐵}) → (𝐴 = (𝐵 ∩ ∩ 𝑣) ↔ 𝐴 = (𝐵 ∩ ∩ (𝑤 ∖ {𝐵})))) |
77 | 76 | rspcev 3282 |
. . . . . . 7
⊢ (((𝑤 ∖ {𝐵}) ∈ (𝒫 𝐶 ∩ Fin) ∧ 𝐴 = (𝐵 ∩ ∩ (𝑤 ∖ {𝐵}))) → ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣)) |
78 | 31, 73, 77 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ (𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ 𝐴 = ∩ 𝑤)) → ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣)) |
79 | 78 | rexlimdvaa 3014 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → (∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)𝐴 = ∩ 𝑤 → ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣))) |
80 | | ssun1 3738 |
. . . . . . . . . . . 12
⊢ {𝐵} ⊆ ({𝐵} ∪ 𝐶) |
81 | 80 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → {𝐵} ⊆ ({𝐵} ∪ 𝐶)) |
82 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢
(𝒫 𝐶 ∩
Fin) ⊆ 𝒫 𝐶 |
83 | 82 | sseli 3564 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝒫 𝐶 ∩ Fin) → 𝑣 ∈ 𝒫 𝐶) |
84 | | elpwi 4117 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝒫 𝐶 → 𝑣 ⊆ 𝐶) |
85 | | ssun4 3741 |
. . . . . . . . . . . . 13
⊢ (𝑣 ⊆ 𝐶 → 𝑣 ⊆ ({𝐵} ∪ 𝐶)) |
86 | 83, 84, 85 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (𝒫 𝐶 ∩ Fin) → 𝑣 ⊆ ({𝐵} ∪ 𝐶)) |
87 | 86 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑣 ⊆ ({𝐵} ∪ 𝐶)) |
88 | 81, 87 | unssd 3751 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → ({𝐵} ∪ 𝑣) ⊆ ({𝐵} ∪ 𝐶)) |
89 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
90 | 9, 89 | unex 6854 |
. . . . . . . . . . 11
⊢ ({𝐵} ∪ 𝑣) ∈ V |
91 | 90 | elpw 4114 |
. . . . . . . . . 10
⊢ (({𝐵} ∪ 𝑣) ∈ 𝒫 ({𝐵} ∪ 𝐶) ↔ ({𝐵} ∪ 𝑣) ⊆ ({𝐵} ∪ 𝐶)) |
92 | 88, 91 | sylibr 223 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → ({𝐵} ∪ 𝑣) ∈ 𝒫 ({𝐵} ∪ 𝐶)) |
93 | | snfi 7923 |
. . . . . . . . . 10
⊢ {𝐵} ∈ Fin |
94 | | inss2 3796 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐶 ∩
Fin) ⊆ Fin |
95 | 94 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (𝒫 𝐶 ∩ Fin) → 𝑣 ∈ Fin) |
96 | 95 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑣 ∈ Fin) |
97 | | unfi 8112 |
. . . . . . . . . 10
⊢ (({𝐵} ∈ Fin ∧ 𝑣 ∈ Fin) → ({𝐵} ∪ 𝑣) ∈ Fin) |
98 | 93, 96, 97 | sylancr 694 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → ({𝐵} ∪ 𝑣) ∈ Fin) |
99 | 92, 98 | elind 3760 |
. . . . . . . 8
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → ({𝐵} ∪ 𝑣) ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)) |
100 | 61 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑉 → 𝐵 = ∩ {𝐵}) |
101 | 100 | ineq1d 3775 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∩ ∩ 𝑣) = (∩ {𝐵}
∩ ∩ 𝑣)) |
102 | | intun 4444 |
. . . . . . . . . 10
⊢ ∩ ({𝐵}
∪ 𝑣) = (∩ {𝐵}
∩ ∩ 𝑣) |
103 | 101, 102 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∩ ∩ 𝑣) = ∩
({𝐵} ∪ 𝑣)) |
104 | 103 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐵 ∩ ∩ 𝑣) = ∩
({𝐵} ∪ 𝑣)) |
105 | | inteq 4413 |
. . . . . . . . . 10
⊢ (𝑤 = ({𝐵} ∪ 𝑣) → ∩ 𝑤 = ∩
({𝐵} ∪ 𝑣)) |
106 | 105 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑤 = ({𝐵} ∪ 𝑣) → ((𝐵 ∩ ∩ 𝑣) = ∩
𝑤 ↔ (𝐵 ∩ ∩ 𝑣) = ∩
({𝐵} ∪ 𝑣))) |
107 | 106 | rspcev 3282 |
. . . . . . . 8
⊢ ((({𝐵} ∪ 𝑣) ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin) ∧ (𝐵 ∩ ∩ 𝑣) = ∩
({𝐵} ∪ 𝑣)) → ∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)(𝐵 ∩ ∩ 𝑣) = ∩
𝑤) |
108 | 99, 104, 107 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)(𝐵 ∩ ∩ 𝑣) = ∩
𝑤) |
109 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝐴 = (𝐵 ∩ ∩ 𝑣) → (𝐴 = ∩ 𝑤 ↔ (𝐵 ∩ ∩ 𝑣) = ∩
𝑤)) |
110 | 109 | rexbidv 3034 |
. . . . . . 7
⊢ (𝐴 = (𝐵 ∩ ∩ 𝑣) → (∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)𝐴 = ∩ 𝑤 ↔ ∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)(𝐵 ∩ ∩ 𝑣) = ∩
𝑤)) |
111 | 108, 110 | syl5ibrcom 236 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) ∧ 𝑣 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐴 = (𝐵 ∩ ∩ 𝑣) → ∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)𝐴 = ∩ 𝑤)) |
112 | 111 | rexlimdva 3013 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → (∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣) → ∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)𝐴 = ∩ 𝑤)) |
113 | 79, 112 | impbid 201 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → (∃𝑤 ∈ (𝒫 ({𝐵} ∪ 𝐶) ∩ Fin)𝐴 = ∩ 𝑤 ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣))) |
114 | 17, 113 | bitrd 267 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) ∧ 𝐴 ∈ V) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣))) |
115 | 114 | ex 449 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ V → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣)))) |
116 | 2, 7, 115 | pm5.21ndd 368 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣))) |