Step | Hyp | Ref
| Expression |
1 | | uneq2 3256 |
. . 3
⊢ (𝑤 = ∅ → (𝐴 ∪ 𝑤) = (𝐴 ∪ ∅)) |
2 | 1 | eleq1d 2226 |
. 2
⊢ (𝑤 = ∅ → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ ∅) ∈
Fin)) |
3 | | uneq2 3256 |
. . 3
⊢ (𝑤 = 𝑦 → (𝐴 ∪ 𝑤) = (𝐴 ∪ 𝑦)) |
4 | 3 | eleq1d 2226 |
. 2
⊢ (𝑤 = 𝑦 → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin)) |
5 | | uneq2 3256 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐴 ∪ 𝑤) = (𝐴 ∪ (𝑦 ∪ {𝑧}))) |
6 | 5 | eleq1d 2226 |
. 2
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
7 | | uneq2 3256 |
. . 3
⊢ (𝑤 = 𝐵 → (𝐴 ∪ 𝑤) = (𝐴 ∪ 𝐵)) |
8 | 7 | eleq1d 2226 |
. 2
⊢ (𝑤 = 𝐵 → ((𝐴 ∪ 𝑤) ∈ Fin ↔ (𝐴 ∪ 𝐵) ∈ Fin)) |
9 | | un0 3428 |
. . 3
⊢ (𝐴 ∪ ∅) = 𝐴 |
10 | | simp1 982 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ Fin) |
11 | 9, 10 | eqeltrid 2244 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ ∅) ∈ Fin) |
12 | | unass 3265 |
. . . 4
⊢ ((𝐴 ∪ 𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})) |
13 | | simpr 109 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ 𝑦) ∈ Fin) |
14 | | vex 2715 |
. . . . . 6
⊢ 𝑧 ∈ V |
15 | 14 | a1i 9 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → 𝑧 ∈ V) |
16 | | simplrr 526 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → 𝑧 ∈ (𝐵 ∖ 𝑦)) |
17 | 16 | eldifad 3113 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → 𝑧 ∈ 𝐵) |
18 | | simp3 984 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = ∅) |
19 | 18 | ad3antrrr 484 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∩ 𝐵) = ∅) |
20 | | minel 3456 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ¬ 𝑧 ∈ 𝐴) |
21 | 17, 19, 20 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ 𝑧 ∈ 𝐴) |
22 | 16 | eldifbd 3114 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ 𝑧 ∈ 𝑦) |
23 | | ioran 742 |
. . . . . . 7
⊢ (¬
(𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦) ↔ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) |
24 | 21, 22, 23 | sylanbrc 414 |
. . . . . 6
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦)) |
25 | | elun 3249 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦)) |
26 | 24, 25 | sylnibr 667 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ¬ 𝑧 ∈ (𝐴 ∪ 𝑦)) |
27 | | unsnfi 6866 |
. . . . 5
⊢ (((𝐴 ∪ 𝑦) ∈ Fin ∧ 𝑧 ∈ V ∧ ¬ 𝑧 ∈ (𝐴 ∪ 𝑦)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin) |
28 | 13, 15, 26, 27 | syl3anc 1220 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin) |
29 | 12, 28 | eqeltrrid 2245 |
. . 3
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin ∧
(𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
30 | 29 | ex 114 |
. 2
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑦))) → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
31 | | simp2 983 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ Fin) |
32 | 2, 4, 6, 8, 11, 30, 31 | findcard2sd 6840 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ Fin) |