Step | Hyp | Ref
| Expression |
1 | | isfi 6751 |
. . 3
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
2 | 1 | biimpi 120 |
. 2
⊢ (𝐴 ∈ Fin → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
3 | | simplrr 536 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 ≈ 𝑛) |
4 | | simpr 110 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝑛 = ∅) |
5 | 3, 4 | breqtrd 4024 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 ≈ ∅) |
6 | | en0 6785 |
. . . . . 6
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
7 | 5, 6 | sylib 122 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 = ∅) |
8 | | nner 2349 |
. . . . 5
⊢ (𝐴 = ∅ → ¬ 𝐴 ≠ ∅) |
9 | 7, 8 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → ¬ 𝐴 ≠ ∅) |
10 | | n0r 3434 |
. . . . . 6
⊢
(∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) |
11 | 10 | necon2bi 2400 |
. . . . 5
⊢ (𝐴 = ∅ → ¬
∃𝑥 𝑥 ∈ 𝐴) |
12 | 7, 11 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → ¬ ∃𝑥 𝑥 ∈ 𝐴) |
13 | 9, 12 | 2falsed 702 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
14 | | simplrr 536 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) → 𝐴 ≈ 𝑛) |
15 | 14 | adantr 276 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → 𝐴 ≈ 𝑛) |
16 | 15 | ensymd 6773 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → 𝑛 ≈ 𝐴) |
17 | | bren 6737 |
. . . . . . . 8
⊢ (𝑛 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝑛–1-1-onto→𝐴) |
18 | 16, 17 | sylib 122 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → ∃𝑓 𝑓:𝑛–1-1-onto→𝐴) |
19 | | f1of 5453 |
. . . . . . . . . . . 12
⊢ (𝑓:𝑛–1-1-onto→𝐴 → 𝑓:𝑛⟶𝐴) |
20 | 19 | adantl 277 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑓:𝑛⟶𝐴) |
21 | | sucidg 4410 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ω → 𝑚 ∈ suc 𝑚) |
22 | 21 | ad3antlr 493 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑚 ∈ suc 𝑚) |
23 | | simplr 528 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑛 = suc 𝑚) |
24 | 22, 23 | eleqtrrd 2255 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑚 ∈ 𝑛) |
25 | 20, 24 | ffvelrnd 5644 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → (𝑓‘𝑚) ∈ 𝐴) |
26 | | elex2 2751 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑚) ∈ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
27 | 25, 26 | syl 14 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → ∃𝑥 𝑥 ∈ 𝐴) |
28 | 27, 10 | syl 14 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝐴 ≠ ∅) |
29 | 28, 27 | 2thd 175 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ (𝑛 ∈ ω
∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
30 | 18, 29 | exlimddv 1896 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
31 | 30 | ex 115 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) → (𝑛 = suc 𝑚 → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴))) |
32 | 31 | rexlimdva 2592 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (∃𝑚 ∈ ω 𝑛 = suc 𝑚 → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴))) |
33 | 32 | imp 124 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ ∃𝑚 ∈ ω 𝑛 = suc 𝑚) → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
34 | | nn0suc 4597 |
. . . 4
⊢ (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∃𝑚 ∈ ω 𝑛 = suc 𝑚)) |
35 | 34 | ad2antrl 490 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝑛 = ∅ ∨ ∃𝑚 ∈ ω 𝑛 = suc 𝑚)) |
36 | 13, 33, 35 | mpjaodan 798 |
. 2
⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
37 | 2, 36 | rexlimddv 2597 |
1
⊢ (𝐴 ∈ Fin → (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴)) |