Proof of Theorem infssuni
Step | Hyp | Ref
| Expression |
1 | | dfral2 3159 |
. . 3
⊢
(∀𝑥 ∈
𝐵 (𝐴 ∩ 𝑥) ∈ Fin ↔ ¬ ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin) |
2 | | iunfi 8964 |
. . . . . . 7
⊢ ((𝐵 ∈ Fin ∧ ∀𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) ∈ Fin) → ∪ 𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) ∈ Fin) |
3 | | iunin2 4979 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) = (𝐴 ∩ ∪
𝑥 ∈ 𝐵 𝑥) |
4 | 3 | eleq1i 2828 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) ∈ Fin ↔ (𝐴 ∩ ∪
𝑥 ∈ 𝐵 𝑥) ∈ Fin) |
5 | | uniiun 4967 |
. . . . . . . . . . . 12
⊢ ∪ 𝐵 =
∪ 𝑥 ∈ 𝐵 𝑥 |
6 | 5 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ ∪ 𝑥 ∈ 𝐵 𝑥 = ∪ 𝐵 |
7 | 6 | ineq2i 4124 |
. . . . . . . . . 10
⊢ (𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥) = (𝐴 ∩ ∪ 𝐵) |
8 | 7 | eleq1i 2828 |
. . . . . . . . 9
⊢ ((𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥) ∈ Fin ↔ (𝐴 ∩ ∪ 𝐵) ∈ Fin) |
9 | | df-ss 3883 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ ∪ 𝐵
↔ (𝐴 ∩ ∪ 𝐵) =
𝐴) |
10 | | eleq1 2825 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ ∪ 𝐵) =
𝐴 → ((𝐴 ∩ ∪ 𝐵)
∈ Fin ↔ 𝐴 ∈
Fin)) |
11 | | pm2.24 124 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin)) |
12 | 10, 11 | syl6bi 256 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ ∪ 𝐵) =
𝐴 → ((𝐴 ∩ ∪ 𝐵)
∈ Fin → (¬ 𝐴
∈ Fin → ∃𝑥
∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin))) |
13 | 9, 12 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ∪ 𝐵
→ ((𝐴 ∩ ∪ 𝐵)
∈ Fin → (¬ 𝐴
∈ Fin → ∃𝑥
∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin))) |
14 | 13 | com12 32 |
. . . . . . . . 9
⊢ ((𝐴 ∩ ∪ 𝐵)
∈ Fin → (𝐴
⊆ ∪ 𝐵 → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin))) |
15 | 8, 14 | sylbi 220 |
. . . . . . . 8
⊢ ((𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥) ∈ Fin → (𝐴 ⊆ ∪ 𝐵 → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin))) |
16 | 4, 15 | sylbi 220 |
. . . . . . 7
⊢ (∪ 𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) ∈ Fin → (𝐴 ⊆ ∪ 𝐵 → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin))) |
17 | 2, 16 | syl 17 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ ∀𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) ∈ Fin) → (𝐴 ⊆ ∪ 𝐵 → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin))) |
18 | 17 | ex 416 |
. . . . 5
⊢ (𝐵 ∈ Fin →
(∀𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) ∈ Fin → (𝐴 ⊆ ∪ 𝐵 → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin)))) |
19 | 18 | com24 95 |
. . . 4
⊢ (𝐵 ∈ Fin → (¬ 𝐴 ∈ Fin → (𝐴 ⊆ ∪ 𝐵
→ (∀𝑥 ∈
𝐵 (𝐴 ∩ 𝑥) ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin)))) |
20 | 19 | 3imp21 1116 |
. . 3
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵)
→ (∀𝑥 ∈
𝐵 (𝐴 ∩ 𝑥) ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin)) |
21 | 1, 20 | syl5bir 246 |
. 2
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵)
→ (¬ ∃𝑥
∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin)) |
22 | 21 | pm2.18d 127 |
1
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵)
→ ∃𝑥 ∈
𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin) |