gdlopcfv2

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlopcfv2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		gdlopcfv2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		2olt9o	⊢ 2_o ∈ 9_o
4		df-2o	⊢ 2_o = suc 1_o
5	3 4	suceldifsn0	⊢ 2_o ∈ ( 9_o ∖ { ∅ } )
6	5	a1i	⊢ ( 𝜑 → 2_o ∈ ( 9_o ∖ { ∅ } ) )
7	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
8	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
9		fvexd	⊢ ( 𝜑 → ( ℱ₂ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V )
10		1on	⊢ 1_o ∈ On
11		2on	⊢ 2_o ∈ On
12	10 4	eqsucidi	⊢ 1_o ∈ 2_o
13	10 11 12	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 2_o = 𝑛 ) → if ( 𝑛 = 1_o , ( ℱ₁ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2_o , ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3_o , ( ℱ₃ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4_o , ( ℱ₄ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5_o , ( ℱ₅ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6_o , ( ℱ₆ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7_o , ( ℱ₇ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ₈ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) = if ( 𝑛 = 2_o , ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3_o , ( ℱ₃ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4_o , ( ℱ₄ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5_o , ( ℱ₅ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6_o , ( ℱ₆ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7_o , ( ℱ₇ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ₈ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) )
14		eqcom	⊢ ( 2_o = 𝑛 ↔ 𝑛 = 2_o )
15	14	bilani	⊢ ( ( 𝜑 ∧ 2_o = 𝑛 ) → 𝑛 = 2_o )
16	15	iftrued	⊢ ( ( 𝜑 ∧ 2_o = 𝑛 ) → if ( 𝑛 = 2_o , ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3_o , ( ℱ₃ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4_o , ( ℱ₄ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5_o , ( ℱ₅ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6_o , ( ℱ₆ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7_o , ( ℱ₇ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ₈ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) = ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
17	13 16	eqtr2d	⊢ ( ( 𝜑 ∧ 2_o = 𝑛 ) → ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = if ( 𝑛 = 1_o , ( ℱ₁ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2_o , ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3_o , ( ℱ₃ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4_o , ( ℱ₄ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5_o , ( ℱ₅ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6_o , ( ℱ₆ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7_o , ( ℱ₇ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ₈ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )
18		opeq1	⊢ ( 𝐴 = 𝑥 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
19	18	fveq2d	⊢ ( 𝐴 = 𝑥 → ( ℱ₂ ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝑥 ) → ( ℱ₂ ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
21		opeq2	⊢ ( 𝐵 = 𝑦 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
22	21	fveq2d	⊢ ( 𝐵 = 𝑦 → ( ℱ₂ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℱ₂ ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = 𝑦 ) → ( ℱ₂ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℱ₂ ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
24		df-gdlopc	⊢ ℱ = ( 𝑛 ∈ ( 9_o ∖ { ∅ } ) , 𝑥 ∈ V , 𝑦 ∈ V ↦ if ( 𝑛 = 1_o , ( ℱ₁ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2_o , ( ℱ₂ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3_o , ( ℱ₃ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4_o , ( ℱ₄ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5_o , ( ℱ₅ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6_o , ( ℱ₆ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7_o , ( ℱ₇ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ₈ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )
25	6 7 8 9 17 20 23 24	mpt3fvot2d	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 2_o , 𝐴 , 𝐵 ⟩ ) = ( ℱ₂ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
26	1 2	gdlop2fv	⊢ ( 𝜑 → ( ℱ₂ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ∩ E ) )
27	25 26	eqtrd	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 2_o , 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ∩ E ) )

Metamath Proof Explorer

Theorem gdlopcfv2

Proof