Theorem mofeu

Description: The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	mofeu.1	⊢ 𝐺 = ( 𝐴 × 𝐵 )
	mofeu.2	⊢ ( 𝜑 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
	mofeu.3	⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ 𝐵 )
Assertion	mofeu	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		mofeu.1	⊢ 𝐺 = ( 𝐴 × 𝐵 )
2		mofeu.2	⊢ ( 𝜑 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
3		mofeu.3	⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ 𝐵 )
4	2	imp	⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )
5		f00	⊢ ( 𝐹 : 𝐴 ⟶ ∅ ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
6	5	rbaib	⊢ ( 𝐴 = ∅ → ( 𝐹 : 𝐴 ⟶ ∅ ↔ 𝐹 = ∅ ) )
7	4 6	syl	⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → ( 𝐹 : 𝐴 ⟶ ∅ ↔ 𝐹 = ∅ ) )
8		feq3	⊢ ( 𝐵 = ∅ → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ∅ ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ∅ ) )
10		xpeq2	⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
11		xp0	⊢ ( 𝐴 × ∅ ) = ∅
12	10 11	eqtrdi	⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
13	1 12	eqtrid	⊢ ( 𝐵 = ∅ → 𝐺 = ∅ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → 𝐺 = ∅ )
15	14	eqeq2d	⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → ( 𝐹 = 𝐺 ↔ 𝐹 = ∅ ) )
16	7 9 15	3bitr4d	⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = 𝐺 ) )
17		19.42v	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝐵 = { 𝑦 } ) ↔ ( 𝜑 ∧ ∃ 𝑦 𝐵 = { 𝑦 } ) )
18		fconst2g	⊢ ( 𝑦 ∈ V → ( 𝐹 : 𝐴 ⟶ { 𝑦 } ↔ 𝐹 = ( 𝐴 × { 𝑦 } ) ) )
19	18	elv	⊢ ( 𝐹 : 𝐴 ⟶ { 𝑦 } ↔ 𝐹 = ( 𝐴 × { 𝑦 } ) )
20		feq3	⊢ ( 𝐵 = { 𝑦 } → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ { 𝑦 } ) )
21		xpeq2	⊢ ( 𝐵 = { 𝑦 } → ( 𝐴 × 𝐵 ) = ( 𝐴 × { 𝑦 } ) )
22	21	eqeq2d	⊢ ( 𝐵 = { 𝑦 } → ( 𝐹 = ( 𝐴 × 𝐵 ) ↔ 𝐹 = ( 𝐴 × { 𝑦 } ) ) )
23	20 22	bibi12d	⊢ ( 𝐵 = { 𝑦 } → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = ( 𝐴 × 𝐵 ) ) ↔ ( 𝐹 : 𝐴 ⟶ { 𝑦 } ↔ 𝐹 = ( 𝐴 × { 𝑦 } ) ) ) )
24	19 23	mpbiri	⊢ ( 𝐵 = { 𝑦 } → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = ( 𝐴 × 𝐵 ) ) )
25	1	eqeq2i	⊢ ( 𝐹 = 𝐺 ↔ 𝐹 = ( 𝐴 × 𝐵 ) )
26	24 25	bitr4di	⊢ ( 𝐵 = { 𝑦 } → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = 𝐺 ) )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑦 } ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = 𝐺 ) )
28	27	exlimiv	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝐵 = { 𝑦 } ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = 𝐺 ) )
29	17 28	sylbir	⊢ ( ( 𝜑 ∧ ∃ 𝑦 𝐵 = { 𝑦 } ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = 𝐺 ) )
30		mo0sn	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ ( 𝐵 = ∅ ∨ ∃ 𝑦 𝐵 = { 𝑦 } ) )
31	3 30	sylib	⊢ ( 𝜑 → ( 𝐵 = ∅ ∨ ∃ 𝑦 𝐵 = { 𝑦 } ) )
32	16 29 31	mpjaodan	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 = 𝐺 ) )