Proof of Theorem f0rn0
| Step | Hyp | Ref
| Expression |
| 1 | | fdm 6745 |
. . 3
⊢ (𝐸:𝑋⟶𝑌 → dom 𝐸 = 𝑋) |
| 2 | | frn 6743 |
. . . . . . . . 9
⊢ (𝐸:𝑋⟶𝑌 → ran 𝐸 ⊆ 𝑌) |
| 3 | | ralnex 3072 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑌 ¬ 𝑦 ∈ ran 𝐸 ↔ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) |
| 4 | | disj 4450 |
. . . . . . . . . . 11
⊢ ((𝑌 ∩ ran 𝐸) = ∅ ↔ ∀𝑦 ∈ 𝑌 ¬ 𝑦 ∈ ran 𝐸) |
| 5 | | dfss2 3969 |
. . . . . . . . . . . 12
⊢ (ran
𝐸 ⊆ 𝑌 ↔ (ran 𝐸 ∩ 𝑌) = ran 𝐸) |
| 6 | | incom 4209 |
. . . . . . . . . . . . . 14
⊢ (ran
𝐸 ∩ 𝑌) = (𝑌 ∩ ran 𝐸) |
| 7 | 6 | eqeq1i 2742 |
. . . . . . . . . . . . 13
⊢ ((ran
𝐸 ∩ 𝑌) = ran 𝐸 ↔ (𝑌 ∩ ran 𝐸) = ran 𝐸) |
| 8 | | eqtr2 2761 |
. . . . . . . . . . . . . 14
⊢ (((𝑌 ∩ ran 𝐸) = ran 𝐸 ∧ (𝑌 ∩ ran 𝐸) = ∅) → ran 𝐸 = ∅) |
| 9 | 8 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∩ ran 𝐸) = ran 𝐸 → ((𝑌 ∩ ran 𝐸) = ∅ → ran 𝐸 = ∅)) |
| 10 | 7, 9 | sylbi 217 |
. . . . . . . . . . . 12
⊢ ((ran
𝐸 ∩ 𝑌) = ran 𝐸 → ((𝑌 ∩ ran 𝐸) = ∅ → ran 𝐸 = ∅)) |
| 11 | 5, 10 | sylbi 217 |
. . . . . . . . . . 11
⊢ (ran
𝐸 ⊆ 𝑌 → ((𝑌 ∩ ran 𝐸) = ∅ → ran 𝐸 = ∅)) |
| 12 | 4, 11 | biimtrrid 243 |
. . . . . . . . . 10
⊢ (ran
𝐸 ⊆ 𝑌 → (∀𝑦 ∈ 𝑌 ¬ 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅)) |
| 13 | 3, 12 | biimtrrid 243 |
. . . . . . . . 9
⊢ (ran
𝐸 ⊆ 𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅)) |
| 14 | 2, 13 | syl 17 |
. . . . . . . 8
⊢ (𝐸:𝑋⟶𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅)) |
| 15 | 14 | imp 406 |
. . . . . . 7
⊢ ((𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) → ran 𝐸 = ∅) |
| 16 | 15 | adantl 481 |
. . . . . 6
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → ran 𝐸 = ∅) |
| 17 | | dm0rn0 5935 |
. . . . . 6
⊢ (dom
𝐸 = ∅ ↔ ran
𝐸 =
∅) |
| 18 | 16, 17 | sylibr 234 |
. . . . 5
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → dom 𝐸 = ∅) |
| 19 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑋 = dom 𝐸 → (𝑋 = ∅ ↔ dom 𝐸 = ∅)) |
| 20 | 19 | eqcoms 2745 |
. . . . . 6
⊢ (dom
𝐸 = 𝑋 → (𝑋 = ∅ ↔ dom 𝐸 = ∅)) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → (𝑋 = ∅ ↔ dom 𝐸 = ∅)) |
| 22 | 18, 21 | mpbird 257 |
. . . 4
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → 𝑋 = ∅) |
| 23 | 22 | exp32 420 |
. . 3
⊢ (dom
𝐸 = 𝑋 → (𝐸:𝑋⟶𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → 𝑋 = ∅))) |
| 24 | 1, 23 | mpcom 38 |
. 2
⊢ (𝐸:𝑋⟶𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → 𝑋 = ∅)) |
| 25 | 24 | imp 406 |
1
⊢ ((𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) → 𝑋 = ∅) |