Step | Hyp | Ref
| Expression |
1 | | uneq2 3275 |
. . 3
⊢ (𝑤 = ∅ → (𝐴 ∪ 𝑤) = (𝐴 ∪ ∅)) |
2 | 1 | eleq1d 2239 |
. 2
⊢ (𝑤 = ∅ → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ ∅) ∈
Fin)) |
3 | | uneq2 3275 |
. . 3
⊢ (𝑤 = 𝑦 → (𝐴 ∪ 𝑤) = (𝐴 ∪ 𝑦)) |
4 | 3 | eleq1d 2239 |
. 2
⊢ (𝑤 = 𝑦 → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin)) |
5 | | uneq2 3275 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐴 ∪ 𝑤) = (𝐴 ∪ (𝑦 ∪ {𝑧}))) |
6 | 5 | eleq1d 2239 |
. 2
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
7 | | uneq2 3275 |
. . 3
⊢ (𝑤 = 𝐵 → (𝐴 ∪ 𝑤) = (𝐴 ∪ 𝐵)) |
8 | 7 | eleq1d 2239 |
. 2
⊢ (𝑤 = 𝐵 → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ 𝐵) ∈ Fin)) |
9 | | un0 3448 |
. . 3
⊢ (𝐴 ∪ ∅) = 𝐴 |
10 | | simp1 992 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ Fin) |
11 | 9, 10 | eqeltrid 2257 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ ∅) ∈ Fin) |
12 | | unass 3284 |
. . . 4
⊢ ((𝐴 ∪ 𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})) |
13 | | simpr 109 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ 𝑦) ∈ Fin) |
14 | | vex 2733 |
. . . . . 6
⊢ 𝑧 ∈ V |
15 | 14 | a1i 9 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → 𝑧 ∈ V) |
16 | | simplrr 531 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → 𝑧 ∈ (𝐵 ∖ 𝑦)) |
17 | 16 | eldifad 3132 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → 𝑧 ∈ 𝐵) |
18 | | simp3 994 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = ∅) |
19 | 18 | ad3antrrr 489 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∩ 𝐵) = ∅) |
20 | | minel 3476 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ¬ 𝑧 ∈ 𝐴) |
21 | 17, 19, 20 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ 𝑧 ∈ 𝐴) |
22 | 16 | eldifbd 3133 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ 𝑧 ∈ 𝑦) |
23 | | ioran 747 |
. . . . . . 7
⊢ (¬
(𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦) ↔ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) |
24 | 21, 22, 23 | sylanbrc 415 |
. . . . . 6
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦)) |
25 | | elun 3268 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦)) |
26 | 24, 25 | sylnibr 672 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ 𝑧 ∈ (𝐴 ∪ 𝑦)) |
27 | | unsnfi 6896 |
. . . . 5
⊢ (((𝐴 ∪ 𝑦) ∈ Fin ∧ 𝑧 ∈ V ∧ ¬ 𝑧 ∈ (𝐴 ∪ 𝑦)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin) |
28 | 13, 15, 26, 27 | syl3anc 1233 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin) |
29 | 12, 28 | eqeltrrid 2258 |
. . 3
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
30 | 29 | ex 114 |
. 2
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
31 | | simp2 993 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ Fin) |
32 | 2, 4, 6, 8, 11, 30, 31 | findcard2sd 6870 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ Fin) |