Theorem gdlopcfv1

Description: The value of the combined Gödel operations function when its first argument is 1. (Contributed by BTernaryTau, 19-Oct-2026)

	Ref	Expression
Hypotheses	gdlopcfv1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gdlopcfv1.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	gdlopcfv1	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 1o , 𝐴 , 𝐵 ⟩ ) = { 𝐴 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		gdlopcfv1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		gdlopcfv1.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		1olt9o	⊢ 1o ∈ 9o
4		df-1o	⊢ 1o = suc ∅
5	3 4	suceldifsn0	⊢ 1o ∈ ( 9o ∖ { ∅ } )
6	5	a1i	⊢ ( 𝜑 → 1o ∈ ( 9o ∖ { ∅ } ) )
7	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
8	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
9		fvexd	⊢ ( 𝜑 → ( ℱ1 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V )
10		eqcom	⊢ ( 1o = 𝑛 ↔ 𝑛 = 1o )
11	10	bilani	⊢ ( ( 𝜑 ∧ 1o = 𝑛 ) → 𝑛 = 1o )
12	11	iftrued	⊢ ( ( 𝜑 ∧ 1o = 𝑛 ) → if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) = ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
13	12	eqcomd	⊢ ( ( 𝜑 ∧ 1o = 𝑛 ) → ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )
14		opeq1	⊢ ( 𝐴 = 𝑥 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
15	14	fveq2d	⊢ ( 𝐴 = 𝑥 → ( ℱ1 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝑥 ) → ( ℱ1 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
17		opeq2	⊢ ( 𝐵 = 𝑦 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
18	17	fveq2d	⊢ ( 𝐵 = 𝑦 → ( ℱ1 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℱ1 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = 𝑦 ) → ( ℱ1 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℱ1 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
20		df-gdlopc	⊢ ℱ = ( 𝑛 ∈ ( 9o ∖ { ∅ } ) , 𝑥 ∈ V , 𝑦 ∈ V ↦ if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )
21	6 7 8 9 13 16 19 20	mpt3fvot2d	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 1o , 𝐴 , 𝐵 ⟩ ) = ( ℱ1 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
22	1 2	gdlop1fv	⊢ ( 𝜑 → ( ℱ1 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { 𝐴 , 𝐵 } )
23	21 22	eqtrd	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 1o , 𝐴 , 𝐵 ⟩ ) = { 𝐴 , 𝐵 } )