| Step | Hyp | Ref
| Expression |
| 1 | | relsdom 8992 |
. . . . . . 7
⊢ Rel
≺ |
| 2 | 1 | brrelex2i 5742 |
. . . . . 6
⊢ (∅
≺ 𝐵 → 𝐵 ∈ V) |
| 3 | | 0sdomg 9144 |
. . . . . . 7
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔ 𝐵 ≠ ∅)) |
| 4 | | n0 4353 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐵) |
| 5 | 3, 4 | bitrdi 287 |
. . . . . 6
⊢ (𝐵 ∈ V → (∅
≺ 𝐵 ↔
∃𝑧 𝑧 ∈ 𝐵)) |
| 6 | 2, 5 | syl 17 |
. . . . 5
⊢ (∅
≺ 𝐵 → (∅
≺ 𝐵 ↔
∃𝑧 𝑧 ∈ 𝐵)) |
| 7 | 6 | ibi 267 |
. . . 4
⊢ (∅
≺ 𝐵 →
∃𝑧 𝑧 ∈ 𝐵) |
| 8 | | domfi 9229 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ Fin) |
| 9 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ Fin) |
| 10 | | brdomi 8999 |
. . . . . . . 8
⊢ (𝐵 ≼ 𝐴 → ∃𝑔 𝑔:𝐵–1-1→𝐴) |
| 11 | | f1fn 6805 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔 Fn 𝐵) |
| 12 | | fnfi 9218 |
. . . . . . . . . . . 12
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → 𝑔 ∈ Fin) |
| 13 | 11, 12 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝑔:𝐵–1-1→𝐴 ∧ 𝐵 ∈ Fin) → 𝑔 ∈ Fin) |
| 14 | 13 | ex 412 |
. . . . . . . . . 10
⊢ (𝑔:𝐵–1-1→𝐴 → (𝐵 ∈ Fin → 𝑔 ∈ Fin)) |
| 15 | | cnvfi 9216 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ Fin → ◡𝑔 ∈ Fin) |
| 16 | | diffi 9215 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Fin → (𝐴 ∖ ran 𝑔) ∈ Fin) |
| 17 | | snfi 9083 |
. . . . . . . . . . . . . . 15
⊢ {𝑧} ∈ Fin |
| 18 | | xpfi 9358 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∖ ran 𝑔) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ Fin) |
| 19 | 16, 17, 18 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Fin → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ Fin) |
| 20 | | unfi 9211 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑔 ∈ Fin ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ Fin) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ Fin) |
| 21 | 15, 19, 20 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ Fin ∧ 𝐴 ∈ Fin) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ Fin) |
| 22 | | df-f1 6566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔)) |
| 23 | 22 | simprbi 496 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔:𝐵–1-1→𝐴 → Fun ◡𝑔) |
| 24 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑧 ∈ V |
| 25 | 24 | fconst 6794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} |
| 26 | | ffun 6739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) |
| 27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ Fun
((𝐴 ∖ ran 𝑔) × {𝑧}) |
| 28 | 23, 27 | jctir 520 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:𝐵–1-1→𝐴 → (Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))) |
| 29 | | df-rn 5696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran 𝑔 = dom ◡𝑔 |
| 30 | 29 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom ◡𝑔 = ran 𝑔 |
| 31 | 24 | snnz 4776 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑧} ≠ ∅ |
| 32 | | dmxp 5939 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑧} ≠ ∅ → dom
((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)) |
| 33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔) |
| 34 | 30, 33 | ineq12i 4218 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) |
| 35 | | disjdif 4472 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅ |
| 36 | 34, 35 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅ |
| 37 | | funun 6612 |
. . . . . . . . . . . . . . . . 17
⊢ (((Fun
◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧}))) |
| 38 | 28, 36, 37 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝐵–1-1→𝐴 → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧}))) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧}))) |
| 40 | | dmun 5921 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
(◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) |
| 41 | 29 | uneq1i 4164 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) |
| 42 | 33 | uneq2i 4165 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) |
| 43 | 40, 41, 42 | 3eqtr2i 2771 |
. . . . . . . . . . . . . . . . 17
⊢ dom
(◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) |
| 44 | | f1f 6804 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔:𝐵⟶𝐴) |
| 45 | 44 | frnd 6744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔:𝐵–1-1→𝐴 → ran 𝑔 ⊆ 𝐴) |
| 46 | | undif 4482 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
𝑔 ⊆ 𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴) |
| 47 | 45, 46 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:𝐵–1-1→𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴) |
| 48 | 43, 47 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝐵–1-1→𝐴 → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴) |
| 49 | 48 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴) |
| 50 | | df-fn 6564 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)) |
| 51 | 39, 49, 50 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴) |
| 52 | | rnun 6165 |
. . . . . . . . . . . . . . 15
⊢ ran
(◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) |
| 53 | | dfdm4 5906 |
. . . . . . . . . . . . . . . . . 18
⊢ dom 𝑔 = ran ◡𝑔 |
| 54 | | f1dm 6808 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔:𝐵–1-1→𝐴 → dom 𝑔 = 𝐵) |
| 55 | 53, 54 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:𝐵–1-1→𝐴 → ran ◡𝑔 = 𝐵) |
| 56 | 55 | uneq1d 4167 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝐵–1-1→𝐴 → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))) |
| 57 | | xpeq1 5699 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧})) |
| 58 | | 0xp 5784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∅
× {𝑧}) =
∅ |
| 59 | 57, 58 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅) |
| 60 | 59 | rneqd 5949 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅) |
| 61 | | rn0 5936 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ran
∅ = ∅ |
| 62 | 60, 61 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅) |
| 63 | | 0ss 4400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
⊆ 𝐵 |
| 64 | 62, 63 | eqsstrdi 4028 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵) |
| 65 | 64 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)) |
| 66 | | rnxp 6190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧}) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧}) |
| 68 | | snssi 4808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝐵 → {𝑧} ⊆ 𝐵) |
| 69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵) |
| 70 | 67, 69 | eqsstrd 4018 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵) |
| 71 | 70 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)) |
| 72 | 65, 71 | pm2.61ine 3025 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵) |
| 73 | | ssequn2 4189 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵) |
| 74 | 72, 73 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵) |
| 75 | 56, 74 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵) |
| 76 | 52, 75 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵) |
| 77 | | df-fo 6567 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 ↔ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)) |
| 78 | 51, 76, 77 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵) |
| 79 | | foeq1 6816 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴–onto→𝐵 ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵)) |
| 80 | 79 | spcegv 3597 |
. . . . . . . . . . . . 13
⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ Fin → ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵)) |
| 81 | 21, 78, 80 | syl2im 40 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ Fin ∧ 𝐴 ∈ Fin) → ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)) |
| 82 | 81 | expcomd 416 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝑔:𝐵–1-1→𝐴 → (𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))) |
| 83 | 82 | com12 32 |
. . . . . . . . . 10
⊢ (𝑔:𝐵–1-1→𝐴 → ((𝑔 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))) |
| 84 | 14, 83 | syland 603 |
. . . . . . . . 9
⊢ (𝑔:𝐵–1-1→𝐴 → ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))) |
| 85 | 84 | exlimiv 1930 |
. . . . . . . 8
⊢
(∃𝑔 𝑔:𝐵–1-1→𝐴 → ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))) |
| 86 | 10, 85 | syl 17 |
. . . . . . 7
⊢ (𝐵 ≼ 𝐴 → ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))) |
| 87 | 86 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))) |
| 88 | 8, 9, 87 | mp2and 699 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → (𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵)) |
| 89 | 88 | exlimdv 1933 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → (∃𝑧 𝑧 ∈ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵)) |
| 90 | 7, 89 | syl5 34 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → (∅ ≺ 𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵)) |
| 91 | 90 | 3impia 1118 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ ∅ ≺ 𝐵) → ∃𝑓 𝑓:𝐴–onto→𝐵) |
| 92 | 91 | 3com23 1127 |
1
⊢ ((𝐴 ∈ Fin ∧ ∅
≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) |