Proof of Theorem fodomfibOLD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fof 6819 | . . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→𝐵 → 𝑓:𝐴⟶𝐵) | 
| 2 | 1 | fdmd 6745 | . . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → dom 𝑓 = 𝐴) | 
| 3 | 2 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐴 = ∅)) | 
| 4 |  | dm0rn0 5934 | . . . . . . . . . . . 12
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) | 
| 5 |  | forn 6822 | . . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) | 
| 6 | 5 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→𝐵 → (ran 𝑓 = ∅ ↔ 𝐵 = ∅)) | 
| 7 | 4, 6 | bitrid 283 | . . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→𝐵 → (dom 𝑓 = ∅ ↔ 𝐵 = ∅)) | 
| 8 | 3, 7 | bitr3d 281 | . . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 = ∅ ↔ 𝐵 = ∅)) | 
| 9 | 8 | necon3bid 2984 | . . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) | 
| 10 | 9 | biimpac 478 | . . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) | 
| 11 | 10 | adantll 714 | . . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≠ ∅) | 
| 12 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑓 ∈ V | 
| 13 | 12 | rnex 7933 | . . . . . . . . . . 11
⊢ ran 𝑓 ∈ V | 
| 14 | 5, 13 | eqeltrrdi 2849 | . . . . . . . . . 10
⊢ (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V) | 
| 15 | 14 | adantl 481 | . . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ∈ V) | 
| 16 |  | 0sdomg 9145 | . . . . . . . . 9
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔ 𝐵 ≠ ∅)) | 
| 17 | 15, 16 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) | 
| 18 | 17 | adantlr 715 | . . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅)) | 
| 19 | 11, 18 | mpbird 257 | . . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴–onto→𝐵) → ∅ ≺ 𝐵) | 
| 20 | 19 | ex 412 | . . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → ∅ ≺ 𝐵)) | 
| 21 |  | fodomfi 9351 | . . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) | 
| 22 | 21 | ex 412 | . . . . . 6
⊢ (𝐴 ∈ Fin → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) | 
| 24 | 20, 23 | jcad 512 | . . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) | 
| 25 | 24 | exlimdv 1932 | . . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) →
(∃𝑓 𝑓:𝐴–onto→𝐵 → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) | 
| 26 | 25 | expimpd 453 | . 2
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) → (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) | 
| 27 |  | sdomdomtr 9151 | . . . 4
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∅ ≺ 𝐴) | 
| 28 |  | 0sdomg 9145 | . . . 4
⊢ (𝐴 ∈ Fin → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) | 
| 29 | 27, 28 | imbitrid 244 | . . 3
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≠ ∅)) | 
| 30 |  | fodomr 9169 | . . 3
⊢ ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) | 
| 31 | 29, 30 | jca2 513 | . 2
⊢ (𝐴 ∈ Fin → ((∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → (𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵))) | 
| 32 | 26, 31 | impbid 212 | 1
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) |