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

Metamath Proof Explorer

Theorem qliftval

Description: The value of the function F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 ⊢ F = ran ⁡ x ∈ X ⟼ x R A
qlift.2 ⊢ φ ∧ x ∈ X → A ∈ Y
qlift.3 ⊢ φ → R Er X
qlift.4 ⊢ φ → X ∈ V
qliftval.4 ⊢ x = C → A = B
qliftval.6 ⊢ φ → Fun ⁡ F
Assertion qliftval ⊢ φ ∧ C ∈ X → F ⁡ C R = B

Proof

Step Hyp Ref Expression
1 qlift.1 ⊢ F = ran ⁡ x ∈ X ⟼ x R A
2 qlift.2 ⊢ φ ∧ x ∈ X → A ∈ Y
3 qlift.3 ⊢ φ → R Er X
4 qlift.4 ⊢ φ → X ∈ V
5 qliftval.4 ⊢ x = C → A = B
6 qliftval.6 ⊢ φ → Fun ⁡ F
7 1 2 3 4 qliftlem ⊢ φ ∧ x ∈ X → x R ∈ X / R
8 eceq1 ⊢ x = C → x R = C R
9 1 7 2 8 5 6 fliftval ⊢ φ ∧ C ∈ X → F ⁡ C R = B