Proof of Theorem fodomb
Step | Hyp | Ref
| Expression |
1 | | fof 6115 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → 𝑓:𝐴⟶𝐵) |
2 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → dom 𝑓 = 𝐴) |
4 | 3 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐴 = ∅)) |
5 | | dm0rn0 5342 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
6 | | forn 6118 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
7 | 6 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (ran 𝑓 = ∅ ↔ 𝐵 = ∅)) |
8 | 5, 7 | syl5bb 272 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐵 = ∅)) |
9 | 4, 8 | bitr3d 270 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 = ∅ ↔ 𝐵 = ∅)) |
10 | 9 | necon3bid 2838 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) |
11 | 10 | biimpac 503 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) |
12 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
13 | 12 | dmex 7099 |
. . . . . . . . . . 11
⊢ dom 𝑓 ∈ V |
14 | 3, 13 | syl6eqelr 2710 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → 𝐴 ∈ V) |
15 | | fornex 7135 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V)) |
16 | 14, 15 | mpcom 38 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V) |
17 | | 0sdomg 8089 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
19 | 18 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
20 | 11, 19 | mpbird 247 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → ∅ ≺ 𝐵) |
21 | 20 | ex 450 |
. . . . 5
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → ∅ ≺ 𝐵)) |
22 | | fodomg 9345 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
23 | 14, 22 | mpcom 38 |
. . . . . 6
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴) |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
25 | 21, 24 | jcad 555 |
. . . 4
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
26 | 25 | exlimdv 1861 |
. . 3
⊢ (𝐴 ≠ ∅ →
(∃𝑓 𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
27 | 26 | imp 445 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)) |
28 | | sdomdomtr 8093 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∅ ≺ 𝐴) |
29 | | reldom 7961 |
. . . . . . 7
⊢ Rel
≼ |
30 | 29 | brrelex2i 5159 |
. . . . . 6
⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V) |
31 | 30 | adantl 482 |
. . . . 5
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V) |
32 | | 0sdomg 8089 |
. . . . 5
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
34 | 28, 33 | mpbid 222 |
. . 3
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≠ ∅) |
35 | | fodomr 8111 |
. . 3
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) |
36 | 34, 35 | jca 554 |
. 2
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵)) |
37 | 27, 36 | impbii 199 |
1
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)) |