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

Metamath Proof Explorer

Theorem qliftfuns

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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion qliftfuns ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑦 ∀ 𝑧 ( 𝑦 𝑅 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 qlift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
2 qlift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
3 qlift.3 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
4 qlift.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5 nfcv ⊢ Ⅎ 𝑦 ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩
6 nfcv ⊢ Ⅎ 𝑥 [ 𝑦 ] 𝑅
7 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴
8 6 7 nfop ⊢ Ⅎ 𝑥 ⟨ [ 𝑦 ] 𝑅 , ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ⟩
9 eceq1 ⊢ ( 𝑥 = 𝑦 → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 )
10 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
11 9 10 opeq12d ⊢ ( 𝑥 = 𝑦 → ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ = ⟨ [ 𝑦 ] 𝑅 , ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ⟩ )
12 5 8 11 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ ) = ( 𝑦 ∈ 𝑋 ↦ ⟨ [ 𝑦 ] 𝑅 , ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ⟩ )
13 12 rneqi ⊢ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ ) = ran ( 𝑦 ∈ 𝑋 ↦ ⟨ [ 𝑦 ] 𝑅 , ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ⟩ )
14 1 13 eqtri ⊢ 𝐹 = ran ( 𝑦 ∈ 𝑋 ↦ ⟨ [ 𝑦 ] 𝑅 , ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ⟩ )
15 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑌 )
16 7 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑌
17 10 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑌 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑌 ) )
18 16 17 rspc ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑌 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑌 ) )
19 15 18 mpan9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑌 )
20 csbeq1 ⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
21 14 19 3 4 20 qliftfun ⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑦 ∀ 𝑧 ( 𝑦 𝑅 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) ) )