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