Proof of Theorem fodomfib
Step | Hyp | Ref
| Expression |
1 | | fof 6028 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→𝐵 → 𝑓:𝐴⟶𝐵) |
2 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → dom 𝑓 = 𝐴) |
4 | 3 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐴 = ∅)) |
5 | | dm0rn0 5263 |
. . . . . . . . . . . 12
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
6 | | forn 6031 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
7 | 6 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → (ran 𝑓 = ∅ ↔ 𝐵 = ∅)) |
8 | 5, 7 | syl5bb 271 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐵 = ∅)) |
9 | 4, 8 | bitr3d 269 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 = ∅ ↔ 𝐵 = ∅)) |
10 | 9 | necon3bid 2826 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) |
11 | 10 | biimpac 502 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) |
12 | 11 | adantll 746 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) |
13 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
14 | 13 | rnex 6992 |
. . . . . . . . . . 11
⊢ ran 𝑓 ∈ V |
15 | 6, 14 | syl6eqelr 2697 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V) |
16 | 15 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ∈ V) |
17 | | 0sdomg 7974 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
19 | 18 | adantlr 747 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
20 | 12, 19 | mpbird 246 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → ∅ ≺ 𝐵) |
21 | 20 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → ∅ ≺ 𝐵)) |
22 | | fodomfi 8124 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |
23 | 22 | ex 449 |
. . . . . 6
⊢ (𝐴 ∈ Fin → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
25 | 21, 24 | jcad 554 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
26 | 25 | exlimdv 1848 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) →
(∃𝑓 𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
27 | 26 | expimpd 627 |
. 2
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
28 | | sdomdomtr 7978 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∅ ≺ 𝐴) |
29 | | 0sdomg 7974 |
. . . 4
⊢ (𝐴 ∈ Fin → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
30 | 28, 29 | syl5ib 233 |
. . 3
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≠ ∅)) |
31 | | fodomr 7996 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) |
32 | 31 | a1i 11 |
. . 3
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)) |
33 | 30, 32 | jcad 554 |
. 2
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵))) |
34 | 27, 33 | impbid 201 |
1
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |