Theorem gdlop4fv

Description: The value of the fourth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026)

	Ref	Expression
Hypotheses	gdlop4fv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gdlop4fv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	gdlop4fv	⊢ ( 𝜑 → ( ℱ4 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		gdlop4fv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		gdlop4fv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
4	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
5	1	resexd	⊢ ( 𝜑 → ( 𝐴 ↾ 𝐵 ) ∈ V )
6		reseq1	⊢ ( 𝐴 = 𝑥 → ( 𝐴 ↾ 𝑦 ) = ( 𝑥 ↾ 𝑦 ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝑥 ) → ( 𝐴 ↾ 𝑦 ) = ( 𝑥 ↾ 𝑦 ) )
8		reseq2	⊢ ( 𝐵 = 𝑦 → ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ↾ 𝑦 ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = 𝑦 ) → ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ↾ 𝑦 ) )
10		df-gdlop4	⊢ ℱ4 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ↾ 𝑦 ) )
11	3 4 5 7 9 10	mpofvop2d	⊢ ( 𝜑 → ( ℱ4 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ↾ 𝐵 ) )