Proof of Theorem fodomb
Step | Hyp | Ref
| Expression |
1 | | fof 6028 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → 𝑓:𝐴⟶𝐵) |
2 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → dom 𝑓 = 𝐴) |
4 | 3 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐴 = ∅)) |
5 | | dm0rn0 5263 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
6 | | forn 6031 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
7 | 6 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (ran 𝑓 = ∅ ↔ 𝐵 = ∅)) |
8 | 5, 7 | syl5bb 271 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐵 = ∅)) |
9 | 4, 8 | bitr3d 269 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 = ∅ ↔ 𝐵 = ∅)) |
10 | 9 | necon3bid 2826 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) |
11 | 10 | biimpac 502 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) |
12 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
13 | 12 | dmex 6991 |
. . . . . . . . . . 11
⊢ dom 𝑓 ∈ V |
14 | 3, 13 | syl6eqelr 2697 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → 𝐴 ∈ V) |
15 | | fornex 7028 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V)) |
16 | 14, 15 | mpcom 37 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V) |
17 | | 0sdomg 7974 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
20 | 11, 19 | mpbird 246 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → ∅ ≺ 𝐵) |
21 | 20 | ex 449 |
. . . . 5
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → ∅ ≺ 𝐵)) |
22 | | fodomg 9228 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
23 | 14, 22 | mpcom 37 |
. . . . . 6
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴) |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
25 | 21, 24 | jcad 554 |
. . . 4
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
26 | 25 | exlimdv 1848 |
. . 3
⊢ (𝐴 ≠ ∅ →
(∃𝑓 𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
27 | 26 | imp 444 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)) |
28 | | sdomdomtr 7978 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∅ ≺ 𝐴) |
29 | | reldom 7847 |
. . . . . . 7
⊢ Rel
≼ |
30 | 29 | brrelex2i 5083 |
. . . . . 6
⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V) |
31 | 30 | adantl 481 |
. . . . 5
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V) |
32 | | 0sdomg 7974 |
. . . . 5
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
34 | 28, 33 | mpbid 221 |
. . 3
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≠ ∅) |
35 | | fodomr 7996 |
. . 3
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) |
36 | 34, 35 | jca 553 |
. 2
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵)) |
37 | 27, 36 | impbii 198 |
1
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)) |