Step | Hyp | Ref
| Expression |
1 | | isfi 6735 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
2 | 1 | biimpi 119 |
. . 3
⊢ (𝐴 ∈ Fin → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
3 | 2 | adantr 274 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
4 | | elex2 2746 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
5 | 4 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → ∃𝑥 𝑥 ∈ 𝐴) |
6 | | fin0 6859 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin → (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴)) |
7 | 6 | adantr 274 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
8 | 5, 7 | mpbird 166 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → 𝐴 ≠ ∅) |
9 | 8 | adantr 274 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → 𝐴 ≠ ∅) |
10 | 9 | neneqd 2361 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → ¬ 𝐴 = ∅) |
11 | | simplrr 531 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 ≈ 𝑛) |
12 | | en0 6769 |
. . . . . . . . 9
⊢ (𝑛 ≈ ∅ ↔ 𝑛 = ∅) |
13 | 12 | biimpri 132 |
. . . . . . . 8
⊢ (𝑛 = ∅ → 𝑛 ≈
∅) |
14 | 13 | adantl 275 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝑛 ≈ ∅) |
15 | | entr 6758 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝑛 ∧ 𝑛 ≈ ∅) → 𝐴 ≈ ∅) |
16 | 11, 14, 15 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 ≈ ∅) |
17 | | en0 6769 |
. . . . . 6
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
18 | 16, 17 | sylib 121 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 = ∅) |
19 | 10, 18 | mtand 660 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → ¬ 𝑛 = ∅) |
20 | | nn0suc 4586 |
. . . . . 6
⊢ (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∃𝑚 ∈ ω 𝑛 = suc 𝑚)) |
21 | 20 | orcomd 724 |
. . . . 5
⊢ (𝑛 ∈ ω →
(∃𝑚 ∈ ω
𝑛 = suc 𝑚 ∨ 𝑛 = ∅)) |
22 | 21 | ad2antrl 487 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (∃𝑚 ∈ ω 𝑛 = suc 𝑚 ∨ 𝑛 = ∅)) |
23 | 19, 22 | ecased 1344 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → ∃𝑚 ∈ ω 𝑛 = suc 𝑚) |
24 | | nnfi 6846 |
. . . . 5
⊢ (𝑚 ∈ ω → 𝑚 ∈ Fin) |
25 | 24 | ad2antrl 487 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → 𝑚 ∈ Fin) |
26 | | simprl 526 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → 𝑚 ∈ ω) |
27 | | simplrr 531 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → 𝐴 ≈ 𝑛) |
28 | | breq2 3991 |
. . . . . . 7
⊢ (𝑛 = suc 𝑚 → (𝐴 ≈ 𝑛 ↔ 𝐴 ≈ suc 𝑚)) |
29 | 28 | ad2antll 488 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → (𝐴 ≈ 𝑛 ↔ 𝐴 ≈ suc 𝑚)) |
30 | 27, 29 | mpbid 146 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → 𝐴 ≈ suc 𝑚) |
31 | | simpllr 529 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → 𝐵 ∈ 𝐴) |
32 | | dif1en 6853 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ 𝐴 ≈ suc 𝑚 ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ≈ 𝑚) |
33 | 26, 30, 31, 32 | syl3anc 1233 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → (𝐴 ∖ {𝐵}) ≈ 𝑚) |
34 | | enfii 6848 |
. . . 4
⊢ ((𝑚 ∈ Fin ∧ (𝐴 ∖ {𝐵}) ≈ 𝑚) → (𝐴 ∖ {𝐵}) ∈ Fin) |
35 | 25, 33, 34 | syl2anc 409 |
. . 3
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚)) → (𝐴 ∖ {𝐵}) ∈ Fin) |
36 | 23, 35 | rexlimddv 2592 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝐴 ∖ {𝐵}) ∈ Fin) |
37 | 3, 36 | rexlimddv 2592 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ∈ Fin) |