Theorem fliftfund

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
	flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
	flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
	fliftfun.4	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐶 )
	fliftfun.5	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐷 )
	fliftfund.6	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 = 𝐶 ) ) → 𝐵 = 𝐷 )
Assertion	fliftfund	⊢ ( 𝜑 → Fun 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2		flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3		flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4		fliftfun.4	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐶 )
5		fliftfun.5	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐷 )
6		fliftfund.6	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 = 𝐶 ) ) → 𝐵 = 𝐷 )
7	6	3exp2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 → ( 𝑦 ∈ 𝑋 → ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ) ) )
8	7	imp32	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) )
9	8	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) )
10	1 2 3 4 5	fliftfun	⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ) )
11	9 10	mpbird	⊢ ( 𝜑 → Fun 𝐹 )