Proof of Theorem fodomfib
Step | Hyp | Ref
| Expression |
1 | | fof 6115 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→𝐵 → 𝑓:𝐴⟶𝐵) |
2 | | fdm 6051 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → dom 𝑓 = 𝐴) |
4 | 3 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐴 = ∅)) |
5 | | dm0rn0 5342 |
. . . . . . . . . . . 12
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
6 | | forn 6118 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
7 | 6 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → (ran 𝑓 = ∅ ↔ 𝐵 = ∅)) |
8 | 5, 7 | syl5bb 272 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐵 = ∅)) |
9 | 4, 8 | bitr3d 270 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 = ∅ ↔ 𝐵 = ∅)) |
10 | 9 | necon3bid 2838 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) |
11 | 10 | biimpac 503 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) |
12 | 11 | adantll 750 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) |
13 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
14 | 13 | rnex 7100 |
. . . . . . . . . . 11
⊢ ran 𝑓 ∈ V |
15 | 6, 14 | syl6eqelr 2710 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V) |
16 | 15 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ∈ V) |
17 | | 0sdomg 8089 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
19 | 18 | adantlr 751 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
20 | 12, 19 | mpbird 247 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → ∅ ≺ 𝐵) |
21 | 20 | ex 450 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → ∅ ≺ 𝐵)) |
22 | | fodomfi 8239 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |
23 | 22 | ex 450 |
. . . . . 6
⊢ (𝐴 ∈ Fin → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
24 | 23 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
25 | 21, 24 | jcad 555 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
26 | 25 | exlimdv 1861 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) →
(∃𝑓 𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
27 | 26 | expimpd 629 |
. 2
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
28 | | sdomdomtr 8093 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∅ ≺ 𝐴) |
29 | | 0sdomg 8089 |
. . . 4
⊢ (𝐴 ∈ Fin → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
30 | 28, 29 | syl5ib 234 |
. . 3
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≠ ∅)) |
31 | | fodomr 8111 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) |
32 | 31 | a1i 11 |
. . 3
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)) |
33 | 30, 32 | jcad 555 |
. 2
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵))) |
34 | 27, 33 | impbid 202 |
1
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |