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

Metamath Proof Explorer

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 𝐹 )