Theorem fliftfuns

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
	flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
	flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion	fliftfuns	⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2		flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3		flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4		nfcv	⊢ Ⅎ 𝑦 ⟨ 𝐴 , 𝐵 ⟩
5		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴
6		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
7	5 6	nfop	⊢ Ⅎ 𝑥 ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩
8		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
9		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	8 9	opeq12d	⊢ ( 𝑥 = 𝑦 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
11	4 7 10	cbvmpt	⊢ ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑦 ∈ 𝑋 ↦ ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
12	11	rneqi	⊢ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ran ( 𝑦 ∈ 𝑋 ↦ ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
13	1 12	eqtri	⊢ 𝐹 = ran ( 𝑦 ∈ 𝑋 ↦ ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
14	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑅 )
15	5	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅
16	8	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑅 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅 ) )
17	15 16	rspc	⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑅 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅 ) )
18	14 17	mpan9	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅 )
19	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 )
20	6	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆
21	9	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ 𝑆 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆 ) )
22	20 21	rspc	⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆 ) )
23	19 22	mpan9	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆 )
24		csbeq1	⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
25		csbeq1	⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
26	13 18 23 24 25	fliftfun	⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )