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

Metamath Proof Explorer

Theorem qliftf

Description: The domain and codomain of the function F . (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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion qliftf ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ( 𝑋 / 𝑅 ) ⟶ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 qlift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
2 qlift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
3 qlift.3 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
4 qlift.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5 1 2 3 4 qliftlem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] 𝑅 ∈ ( 𝑋 / 𝑅 ) )
6 1 5 2 fliftf ⊢ ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) ⟶ 𝑌 ) )
7 df-qs ⊢ ( 𝑋 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = [ 𝑥 ] 𝑅 }
8 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 )
9 8 rnmpt ⊢ ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = [ 𝑥 ] 𝑅 }
10 7 9 eqtr4i ⊢ ( 𝑋 / 𝑅 ) = ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 )
11 10 a1i ⊢ ( 𝜑 → ( 𝑋 / 𝑅 ) = ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) )
12 11 feq2d ⊢ ( 𝜑 → ( 𝐹 : ( 𝑋 / 𝑅 ) ⟶ 𝑌 ↔ 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) ⟶ 𝑌 ) )
13 6 12 bitr4d ⊢ ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ( 𝑋 / 𝑅 ) ⟶ 𝑌 ) )