Metamath Proof Explorer

Theorem f0rn0

Description: If there is no element in the range of a function, its domain must be empty. (Contributed by Alexander van der Vekens, 12-Jul-2018)

Ref Expression
Assertion f0rn0 ( ( 𝐸 : 𝑋 ⟶ 𝑌 ∧ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 ) → 𝑋 = ∅ )

Proof

Step Hyp Ref Expression
1 fdm ⊢ ( 𝐸 : 𝑋 ⟶ 𝑌 → dom 𝐸 = 𝑋 )
2 frn ⊢ ( 𝐸 : 𝑋 ⟶ 𝑌 → ran 𝐸 ⊆ 𝑌 )
3 ralnex ⊢ ( ∀ 𝑦 ∈ 𝑌 ¬ 𝑦 ∈ ran 𝐸 ↔ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 )
4 disj ⊢ ( ( 𝑌 ∩ ran 𝐸 ) = ∅ ↔ ∀ 𝑦 ∈ 𝑌 ¬ 𝑦 ∈ ran 𝐸 )
5 dfss2 ⊢ ( ran 𝐸 ⊆ 𝑌 ↔ ( ran 𝐸 ∩ 𝑌 ) = ran 𝐸 )
6 incom ⊢ ( ran 𝐸 ∩ 𝑌 ) = ( 𝑌 ∩ ran 𝐸 )
7 6 eqeq1i ⊢ ( ( ran 𝐸 ∩ 𝑌 ) = ran 𝐸 ↔ ( 𝑌 ∩ ran 𝐸 ) = ran 𝐸 )
8 eqtr2 ⊢ ( ( ( 𝑌 ∩ ran 𝐸 ) = ran 𝐸 ∧ ( 𝑌 ∩ ran 𝐸 ) = ∅ ) → ran 𝐸 = ∅ )
9 8 ex ⊢ ( ( 𝑌 ∩ ran 𝐸 ) = ran 𝐸 → ( ( 𝑌 ∩ ran 𝐸 ) = ∅ → ran 𝐸 = ∅ ) )
10 7 9 sylbi ⊢ ( ( ran 𝐸 ∩ 𝑌 ) = ran 𝐸 → ( ( 𝑌 ∩ ran 𝐸 ) = ∅ → ran 𝐸 = ∅ ) )
11 5 10 sylbi ⊢ ( ran 𝐸 ⊆ 𝑌 → ( ( 𝑌 ∩ ran 𝐸 ) = ∅ → ran 𝐸 = ∅ ) )
12 4 11 biimtrrid ⊢ ( ran 𝐸 ⊆ 𝑌 → ( ∀ 𝑦 ∈ 𝑌 ¬ 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅ ) )
13 3 12 biimtrrid ⊢ ( ran 𝐸 ⊆ 𝑌 → ( ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅ ) )
14 2 13 syl ⊢ ( 𝐸 : 𝑋 ⟶ 𝑌 → ( ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → ran 𝐸 = ∅ ) )
15 14 imp ⊢ ( ( 𝐸 : 𝑋 ⟶ 𝑌 ∧ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 ) → ran 𝐸 = ∅ )
16 15 adantl ⊢ ( ( dom 𝐸 = 𝑋 ∧ ( 𝐸 : 𝑋 ⟶ 𝑌 ∧ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 ) ) → ran 𝐸 = ∅ )
17 dm0rn0 ⊢ ( dom 𝐸 = ∅ ↔ ran 𝐸 = ∅ )
18 16 17 sylibr ⊢ ( ( dom 𝐸 = 𝑋 ∧ ( 𝐸 : 𝑋 ⟶ 𝑌 ∧ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 ) ) → dom 𝐸 = ∅ )
19 eqeq1 ⊢ ( 𝑋 = dom 𝐸 → ( 𝑋 = ∅ ↔ dom 𝐸 = ∅ ) )
20 19 eqcoms ⊢ ( dom 𝐸 = 𝑋 → ( 𝑋 = ∅ ↔ dom 𝐸 = ∅ ) )
21 20 adantr ⊢ ( ( dom 𝐸 = 𝑋 ∧ ( 𝐸 : 𝑋 ⟶ 𝑌 ∧ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 ) ) → ( 𝑋 = ∅ ↔ dom 𝐸 = ∅ ) )
22 18 21 mpbird ⊢ ( ( dom 𝐸 = 𝑋 ∧ ( 𝐸 : 𝑋 ⟶ 𝑌 ∧ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 ) ) → 𝑋 = ∅ )
23 22 exp32 ⊢ ( dom 𝐸 = 𝑋 → ( 𝐸 : 𝑋 ⟶ 𝑌 → ( ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → 𝑋 = ∅ ) ) )
24 1 23 mpcom ⊢ ( 𝐸 : 𝑋 ⟶ 𝑌 → ( ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 → 𝑋 = ∅ ) )
25 24 imp ⊢ ( ( 𝐸 : 𝑋 ⟶ 𝑌 ∧ ¬ ∃ 𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸 ) → 𝑋 = ∅ )