Step | Hyp | Ref
| Expression |
1 | | fof 6757 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → 𝑓:𝐴⟶𝐵) |
2 | 1 | fdmd 6680 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → dom 𝑓 = 𝐴) |
3 | 2 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐴 = ∅)) |
4 | | dm0rn0 5881 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
5 | | forn 6760 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
6 | 5 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (ran 𝑓 = ∅ ↔ 𝐵 = ∅)) |
7 | 4, 6 | bitrid 283 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐵 = ∅)) |
8 | 3, 7 | bitr3d 281 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 = ∅ ↔ 𝐵 = ∅)) |
9 | 8 | necon3bid 2989 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) |
10 | 9 | biimpac 480 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) |
11 | | vex 3450 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
12 | 11 | dmex 7849 |
. . . . . . . . . . 11
⊢ dom 𝑓 ∈ V |
13 | 2, 12 | eqeltrrdi 2847 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → 𝐴 ∈ V) |
14 | | focdmex 7889 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V)) |
15 | 13, 14 | mpcom 38 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V) |
16 | | 0sdomg 9049 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
18 | 17 | adantl 483 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
19 | 10, 18 | mpbird 257 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → ∅ ≺ 𝐵) |
20 | 19 | ex 414 |
. . . . 5
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → ∅ ≺ 𝐵)) |
21 | | fodomg 10459 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) |
22 | 13, 21 | mpcom 38 |
. . . . 5
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴) |
23 | 20, 22 | jca2 515 |
. . . 4
⊢ (𝐴 ≠ ∅ → (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
24 | 23 | exlimdv 1937 |
. . 3
⊢ (𝐴 ≠ ∅ →
(∃𝑓 𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
25 | 24 | imp 408 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)) |
26 | | sdomdomtr 9055 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∅ ≺ 𝐴) |
27 | | reldom 8890 |
. . . . . . 7
⊢ Rel
≼ |
28 | 27 | brrelex2i 5690 |
. . . . . 6
⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V) |
29 | 28 | adantl 483 |
. . . . 5
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V) |
30 | | 0sdomg 9049 |
. . . . 5
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
32 | 26, 31 | mpbid 231 |
. . 3
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≠ ∅) |
33 | | fodomr 9073 |
. . 3
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) |
34 | 32, 33 | jca 513 |
. 2
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵)) |
35 | 25, 34 | impbii 208 |
1
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)) |