Theorem gdlopcfv8

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

	Ref	Expression
Hypotheses	gdlopcfv8.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gdlopcfv8.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	gdlopcfv8	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 8o , 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ∩ ( Cnv3 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gdlopcfv8.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		gdlopcfv8.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		8olt9o	⊢ 8o ∈ 9o
4		df-8o	⊢ 8o = suc 7o
5	3 4	suceldifsn0	⊢ 8o ∈ ( 9o ∖ { ∅ } )
6	5	a1i	⊢ ( 𝜑 → 8o ∈ ( 9o ∖ { ∅ } ) )
7	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
8	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
9		fvexd	⊢ ( 𝜑 → ( ℱ8 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V )
10		2on	⊢ 2o ∈ On
11		8on	⊢ 8o ∈ On
12		df-3o	⊢ 3o = suc 2o
13	10 12	eqsucidi	⊢ 2o ∈ 3o
14		3on	⊢ 3o ∈ On
15		df-4o	⊢ 4o = suc 3o
16	14 15	eqsucidi	⊢ 3o ∈ 4o
17		4on	⊢ 4o ∈ On
18		df-5o	⊢ 5o = suc 4o
19	17 18	eqsucidi	⊢ 4o ∈ 5o
20		5on	⊢ 5o ∈ On
21		df-6o	⊢ 6o = suc 5o
22	20 21	eqsucidi	⊢ 5o ∈ 6o
23		6on	⊢ 6o ∈ On
24		df-7o	⊢ 7o = suc 6o
25	23 24	eqsucidi	⊢ 6o ∈ 7o
26		7on	⊢ 7o ∈ On
27	26 4	eqsucidi	⊢ 7o ∈ 8o
28	11 25 27	ontr1i	⊢ 6o ∈ 8o
29	11 22 28	ontr1i	⊢ 5o ∈ 8o
30	11 19 29	ontr1i	⊢ 4o ∈ 8o
31	11 16 30	ontr1i	⊢ 3o ∈ 8o
32	11 13 31	ontr1i	⊢ 2o ∈ 8o
33	10 11 32	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) = if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) )
34		1on	⊢ 1o ∈ On
35		df-2o	⊢ 2o = suc 1o
36	34 35	eqsucidi	⊢ 1o ∈ 2o
37	11 36 32	ontr1i	⊢ 1o ∈ 8o
38	34 11 37	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) = if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) )
39	17 11 30	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) = if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) )
40	14 11 31	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) = if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )
41	20 11 29	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) = if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
42	23 11 28	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) = if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
43	26 11 27	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
44	41 42 43	3eqtrrd	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) )
45	39 40 44	3eqtr4rd	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) )
46	33 38 45	3eqtr4rd	⊢ ( ( 𝜑 ∧ 8o = 𝑛 ) → ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )
47		opeq1	⊢ ( 𝐴 = 𝑥 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
48	47	fveq2d	⊢ ( 𝐴 = 𝑥 → ( ℱ8 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
49	48	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝑥 ) → ( ℱ8 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
50		opeq2	⊢ ( 𝐵 = 𝑦 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
51	50	fveq2d	⊢ ( 𝐵 = 𝑦 → ( ℱ8 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℱ8 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
52	51	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = 𝑦 ) → ( ℱ8 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℱ8 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
53		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 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )
54	6 7 8 9 46 49 52 53	mpt3fvot2d	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 8o , 𝐴 , 𝐵 ⟩ ) = ( ℱ8 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
55	1 2	gdlop8fv	⊢ ( 𝜑 → ( ℱ8 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ∩ ( Cnv3 ‘ 𝐵 ) ) )
56	54 55	eqtrd	⊢ ( 𝜑 → ( ℱ ‘ ⟨ 8o , 𝐴 , 𝐵 ⟩ ) = ( 𝐴 ∩ ( Cnv3 ‘ 𝐵 ) ) )