Step | Hyp | Ref
| Expression |
1 | | fdm 6678 |
. . 3
⊢ (𝐸:𝑋⟶𝑌 → dom 𝐸 = 𝑋) |
2 | | frn 6676 |
. . . . . . . . 9
⊢ (𝐸:𝑋⟶𝑌 → ran 𝐸 ⊆ 𝑌) |
3 | | ralnex 3076 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑌 ¬ 𝑦 ∈ ran 𝐸 ↔ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) |
4 | | disj 4408 |
. . . . . . . . . . 11
⊢ ((𝑌 ∩ ran 𝐸) = ∅ ↔ ∀𝑦 ∈ 𝑌 ¬ 𝑦 ∈ ran 𝐸) |
5 | | df-ss 3928 |
. . . . . . . . . . . 12
⊢ (ran
𝐸 ⊆ 𝑌 ↔ (ran 𝐸 ∩ 𝑌) = ran 𝐸) |
6 | | incom 4162 |
. . . . . . . . . . . . . 14
⊢ (ran
𝐸 ∩ 𝑌) = (𝑌 ∩ ran 𝐸) |
7 | 6 | eqeq1i 2742 |
. . . . . . . . . . . . 13
⊢ ((ran
𝐸 ∩ 𝑌) = ran 𝐸 ↔ (𝑌 ∩ ran 𝐸) = ran 𝐸) |
8 | | eqtr2 2761 |
. . . . . . . . . . . . . 14
⊢ (((𝑌 ∩ ran 𝐸) = ran 𝐸 ∧ (𝑌 ∩ ran 𝐸) = ∅) → ran 𝐸 = ∅) |
9 | 8 | ex 414 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∩ ran 𝐸) = ran 𝐸 → ((𝑌 ∩ ran 𝐸) = ∅ → ran 𝐸 = ∅)) |
10 | 7, 9 | sylbi 216 |
. . . . . . . . . . . 12
⊢ ((ran
𝐸 ∩ 𝑌) = ran 𝐸 → ((𝑌 ∩ ran 𝐸) = ∅ → ran 𝐸 = ∅)) |
11 | 5, 10 | sylbi 216 |
. . . . . . . . . . 11
⊢ (ran
𝐸 ⊆ 𝑌 → ((𝑌 ∩ ran 𝐸) = ∅ → ran 𝐸 = ∅)) |
12 | 4, 11 | biimtrrid 242 |
. . . . . . . . . 10
⊢ (ran
𝐸 ⊆ 𝑌 → (∀𝑦 ∈ 𝑌 ¬ 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅)) |
13 | 3, 12 | biimtrrid 242 |
. . . . . . . . 9
⊢ (ran
𝐸 ⊆ 𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅)) |
14 | 2, 13 | syl 17 |
. . . . . . . 8
⊢ (𝐸:𝑋⟶𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅)) |
15 | 14 | imp 408 |
. . . . . . 7
⊢ ((𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) → ran 𝐸 = ∅) |
16 | 15 | adantl 483 |
. . . . . 6
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → ran 𝐸 = ∅) |
17 | | dm0rn0 5881 |
. . . . . 6
⊢ (dom
𝐸 = ∅ ↔ ran
𝐸 =
∅) |
18 | 16, 17 | sylibr 233 |
. . . . 5
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → dom 𝐸 = ∅) |
19 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑋 = dom 𝐸 → (𝑋 = ∅ ↔ dom 𝐸 = ∅)) |
20 | 19 | eqcoms 2745 |
. . . . . 6
⊢ (dom
𝐸 = 𝑋 → (𝑋 = ∅ ↔ dom 𝐸 = ∅)) |
21 | 20 | adantr 482 |
. . . . 5
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → (𝑋 = ∅ ↔ dom 𝐸 = ∅)) |
22 | 18, 21 | mpbird 257 |
. . . 4
⊢ ((dom
𝐸 = 𝑋 ∧ (𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸)) → 𝑋 = ∅) |
23 | 22 | exp32 422 |
. . 3
⊢ (dom
𝐸 = 𝑋 → (𝐸:𝑋⟶𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → 𝑋 = ∅))) |
24 | 1, 23 | mpcom 38 |
. 2
⊢ (𝐸:𝑋⟶𝑌 → (¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → 𝑋 = ∅)) |
25 | 24 | imp 408 |
1
⊢ ((𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) → 𝑋 = ∅) |