Step | Hyp | Ref
| Expression |
1 | | ssfii 6949 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴)) |
2 | 1 | unissd 3818 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ⊆ ∪ (fi‘𝐴)) |
3 | | eluni 3797 |
. . . . 5
⊢ (𝑥 ∈ ∪ (fi‘𝐴) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) |
4 | 3 | biimpi 119 |
. . . 4
⊢ (𝑥 ∈ ∪ (fi‘𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) |
5 | 4 | adantl 275 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) →
∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) |
6 | | simprr 527 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) → 𝑦 ∈ (fi‘𝐴)) |
7 | | elfi2 6947 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑦 ∈ (fi‘𝐴) ↔ ∃𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})𝑦 = ∩
𝑧)) |
8 | 7 | ad2antrr 485 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) → (𝑦 ∈ (fi‘𝐴) ↔ ∃𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})𝑦 = ∩
𝑧)) |
9 | 6, 8 | mpbid 146 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) → ∃𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})𝑦 = ∩
𝑧) |
10 | | simprr 527 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) ∧ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∧ 𝑦 = ∩
𝑧)) → 𝑦 = ∩
𝑧) |
11 | | eldifi 3249 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
→ 𝑧 ∈ (𝒫
𝐴 ∩
Fin)) |
12 | 11 | elin1d 3316 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
→ 𝑧 ∈ 𝒫
𝐴) |
13 | 12 | elpwid 3575 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
→ 𝑧 ⊆ 𝐴) |
14 | 13 | ad2antrl 487 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) ∧ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∧ 𝑦 = ∩
𝑧)) → 𝑧 ⊆ 𝐴) |
15 | | eldifsni 3710 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
→ 𝑧 ≠
∅) |
16 | 11 | elin2d 3317 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
→ 𝑧 ∈
Fin) |
17 | | fin0 6861 |
. . . . . . . . . 10
⊢ (𝑧 ∈ Fin → (𝑧 ≠ ∅ ↔
∃𝑤 𝑤 ∈ 𝑧)) |
18 | 16, 17 | syl 14 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
→ (𝑧 ≠ ∅
↔ ∃𝑤 𝑤 ∈ 𝑧)) |
19 | 15, 18 | mpbid 146 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
→ ∃𝑤 𝑤 ∈ 𝑧) |
20 | 19 | ad2antrl 487 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) ∧ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∧ 𝑦 = ∩
𝑧)) → ∃𝑤 𝑤 ∈ 𝑧) |
21 | | intssuni2m 3853 |
. . . . . . 7
⊢ ((𝑧 ⊆ 𝐴 ∧ ∃𝑤 𝑤 ∈ 𝑧) → ∩ 𝑧 ⊆ ∪ 𝐴) |
22 | 14, 20, 21 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) ∧ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∧ 𝑦 = ∩
𝑧)) → ∩ 𝑧
⊆ ∪ 𝐴) |
23 | 10, 22 | eqsstrd 3183 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) ∧ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∧ 𝑦 = ∩
𝑧)) → 𝑦 ⊆ ∪ 𝐴) |
24 | | simplrl 530 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) ∧ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∧ 𝑦 = ∩
𝑧)) → 𝑥 ∈ 𝑦) |
25 | 23, 24 | sseldd 3148 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) ∧ (𝑧 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∧ 𝑦 = ∩
𝑧)) → 𝑥 ∈ ∪ 𝐴) |
26 | 9, 25 | rexlimddv 2592 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (fi‘𝐴))) → 𝑥 ∈ ∪ 𝐴) |
27 | 5, 26 | exlimddv 1891 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ∪
(fi‘𝐴)) → 𝑥 ∈ ∪ 𝐴) |
28 | 2, 27 | eqelssd 3166 |
1
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 = ∪
(fi‘𝐴)) |