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 𝐹 ↔ ∀ 𝑦 ∀ 𝑧 ( 𝑦 𝑅 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) ) )