Metamath Proof Explorer


Theorem qliftfund

Description: The function F is the unique function defined by F[ x ] = A , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 𝐹 = ran ( 𝑥𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
qlift.2 ( ( 𝜑𝑥𝑋 ) → 𝐴𝑌 )
qlift.3 ( 𝜑𝑅 Er 𝑋 )
qlift.4 ( 𝜑𝑋𝑉 )
qliftfun.4 ( 𝑥 = 𝑦𝐴 = 𝐵 )
qliftfund.6 ( ( 𝜑𝑥 𝑅 𝑦 ) → 𝐴 = 𝐵 )
Assertion qliftfund ( 𝜑 → Fun 𝐹 )

Proof

Step Hyp Ref Expression
1 qlift.1 𝐹 = ran ( 𝑥𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
2 qlift.2 ( ( 𝜑𝑥𝑋 ) → 𝐴𝑌 )
3 qlift.3 ( 𝜑𝑅 Er 𝑋 )
4 qlift.4 ( 𝜑𝑋𝑉 )
5 qliftfun.4 ( 𝑥 = 𝑦𝐴 = 𝐵 )
6 qliftfund.6 ( ( 𝜑𝑥 𝑅 𝑦 ) → 𝐴 = 𝐵 )
7 6 ex ( 𝜑 → ( 𝑥 𝑅 𝑦𝐴 = 𝐵 ) )
8 7 alrimivv ( 𝜑 → ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝐴 = 𝐵 ) )
9 1 2 3 4 5 qliftfun ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝐴 = 𝐵 ) ) )
10 8 9 mpbird ( 𝜑 → Fun 𝐹 )