prfval

Description: Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	prfval.k	⊢ 𝑃 = ( 𝐹 ⟨,⟩_F 𝐺 )
	prfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	prfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	prfval.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	prfval.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
Assertion	prfval	⊢ ( 𝜑 → 𝑃 = ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		prfval.k	⊢ 𝑃 = ( 𝐹 ⟨,⟩_F 𝐺 )
2		prfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		prfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		prfval.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		prfval.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
6		df-prf	⊢ ⟨,⟩_F = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⦋ dom ( 1^st ‘ 𝑓 ) / 𝑏 ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
7	6	a1i	⊢ ( 𝜑 → ⟨,⟩_F = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⦋ dom ( 1^st ‘ 𝑓 ) / 𝑏 ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ ) )
8		fvex	⊢ ( 1^st ‘ 𝑓 ) ∈ V
9	8	dmex	⊢ dom ( 1^st ‘ 𝑓 ) ∈ V
10	9	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → dom ( 1^st ‘ 𝑓 ) ∈ V )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → 𝑓 = 𝐹 )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
13	12	dmeqd	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → dom ( 1^st ‘ 𝑓 ) = dom ( 1^st ‘ 𝐹 ) )
14		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
15		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
16		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
17	15 4 16	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
18	2 14 17	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
19	18	fdmd	⊢ ( 𝜑 → dom ( 1^st ‘ 𝐹 ) = 𝐵 )
20	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → dom ( 1^st ‘ 𝐹 ) = 𝐵 )
21	13 20	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → dom ( 1^st ‘ 𝑓 ) = 𝐵 )
22		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
23		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝐹 )
24	23	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
25	24	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) )
26		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → 𝑔 = 𝐺 )
27	26	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 1^st ‘ 𝑔 ) = ( 1^st ‘ 𝐺 ) )
28	27	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) )
29	25 28	opeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
30	22 29	mpteq12dv	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
31		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) = ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
32	22 22 31	mpoeq123dv	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) )
33	23	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑓 = 𝐹 )
34	33	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ 𝐹 ) )
35	34	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
36	35	dmeqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) = dom ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
37		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
38	17	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
39		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
40		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
41	2 3 37 38 39 40	funcf2	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
42	41	fdmd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → dom ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
43	36 42	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
44	35	fveq1d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) )
45	26	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑔 = 𝐺 )
46	45	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 2^nd ‘ 𝑔 ) = ( 2^nd ‘ 𝐺 ) )
47	46	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) )
48	47	fveq1d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) = ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) )
49	44 48	opeq12d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ = ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ )
50	43 49	mpteq12dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) = ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
51	50	3impa	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) = ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
52	51	mpoeq3dva	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) )
53	32 52	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) )
54	30 53	opeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
55	10 21 54	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ⦋ dom ( 1^st ‘ 𝑓 ) / 𝑏 ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
56	4	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
57	5	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
58		opex	⊢ ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ ∈ V
59	58	a1i	⊢ ( 𝜑 → ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ ∈ V )
60	7 55 56 57 59	ovmpod	⊢ ( 𝜑 → ( 𝐹 ⟨,⟩_F 𝐺 ) = ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
61	1 60	eqtrid	⊢ ( 𝜑 → 𝑃 = ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )

Metamath Proof Explorer

Theorem prfval

Proof