Theorem gdlop7fv

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

	Ref	Expression
Hypotheses	gdlop7fv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gdlop7fv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	gdlop7fv	⊢ ( 𝜑 → ( ℱ7 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ∩ ( Cnv2 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gdlop7fv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		gdlop7fv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
4	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
5		inex1g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ( Cnv2 ‘ 𝐵 ) ) ∈ V )
6	1 5	syl	⊢ ( 𝜑 → ( 𝐴 ∩ ( Cnv2 ‘ 𝐵 ) ) ∈ V )
7		ineq1	⊢ ( 𝐴 = 𝑥 → ( 𝐴 ∩ ( Cnv2 ‘ 𝑦 ) ) = ( 𝑥 ∩ ( Cnv2 ‘ 𝑦 ) ) )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝑥 ) → ( 𝐴 ∩ ( Cnv2 ‘ 𝑦 ) ) = ( 𝑥 ∩ ( Cnv2 ‘ 𝑦 ) ) )
9		fveq2	⊢ ( 𝐵 = 𝑦 → ( Cnv2 ‘ 𝐵 ) = ( Cnv2 ‘ 𝑦 ) )
10	9	ineq2d	⊢ ( 𝐵 = 𝑦 → ( 𝐴 ∩ ( Cnv2 ‘ 𝐵 ) ) = ( 𝐴 ∩ ( Cnv2 ‘ 𝑦 ) ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = 𝑦 ) → ( 𝐴 ∩ ( Cnv2 ‘ 𝐵 ) ) = ( 𝐴 ∩ ( Cnv2 ‘ 𝑦 ) ) )
12		df-gdlop7	⊢ ℱ7 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∩ ( Cnv2 ‘ 𝑦 ) ) )
13	3 4 6 8 11 12	mpofvop2d	⊢ ( 𝜑 → ( ℱ7 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ∩ ( Cnv2 ‘ 𝐵 ) ) )