This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem map0cor

Description: A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024)

		Ref	Expression
	Hypotheses	map0cor.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
		map0cor.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	Assertion	map0cor	⊢ ( 𝜑 → ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ∃ 𝑓 𝑓 : 𝐴 ⟶ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		map0cor.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		map0cor.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		biid	⊢ ( 𝐴 ≠ ∅ ↔ 𝐴 ≠ ∅ )
4	3	necon2bbii	⊢ ( 𝐴 = ∅ ↔ ¬ 𝐴 ≠ ∅ )
5	4	imbi2i	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ( 𝐵 = ∅ → ¬ 𝐴 ≠ ∅ ) )
6		imnan	⊢ ( ( 𝐵 = ∅ → ¬ 𝐴 ≠ ∅ ) ↔ ¬ ( 𝐵 = ∅ ∧ 𝐴 ≠ ∅ ) )
7	5 6	bitri	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ¬ ( 𝐵 = ∅ ∧ 𝐴 ≠ ∅ ) )
8		map0g	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐵 ↑_m 𝐴 ) = ∅ ↔ ( 𝐵 = ∅ ∧ 𝐴 ≠ ∅ ) ) )
9	8	notbid	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ( 𝐵 ↑_m 𝐴 ) = ∅ ↔ ¬ ( 𝐵 = ∅ ∧ 𝐴 ≠ ∅ ) ) )
10	7 9	bitr4id	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ¬ ( 𝐵 ↑_m 𝐴 ) = ∅ ) )
11		neq0	⊢ ( ¬ ( 𝐵 ↑_m 𝐴 ) = ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) )
12	11	a1i	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ( 𝐵 ↑_m 𝐴 ) = ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) ) )
13		elmapg	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐵 ) )
14	13	exbidv	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) ↔ ∃ 𝑓 𝑓 : 𝐴 ⟶ 𝐵 ) )
15	10 12 14	3bitrd	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ∃ 𝑓 𝑓 : 𝐴 ⟶ 𝐵 ) )
16	2 1 15	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ∃ 𝑓 𝑓 : 𝐴 ⟶ 𝐵 ) )