reldmprcof1

Description: The domain of the object part of the pre-composition functor is a relation. (Contributed by Zhi Wang, 2-Nov-2025)

		Ref	Expression
	Assertion	reldmprcof1	⊢ Rel dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		relfunc	⊢ Rel ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) )
2		ovex	⊢ ( 𝑘 ∘_func 𝐹 ) ∈ V
3		eqid	⊢ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) = ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) )
4	2 3	dmmpti	⊢ dom ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) = ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) )
5	4	releqi	⊢ ( Rel dom ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) ↔ Rel ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) )
6	1 5	mpbir	⊢ Rel dom ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) )
7		eqid	⊢ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) = ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) )
8		eqid	⊢ ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) = ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) )
9		simpr	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → 𝐹 ∈ V )
10		simpl	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → 𝑃 ∈ V )
11		eqidd	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( 1^st ‘ 𝑃 ) = ( 1^st ‘ 𝑃 ) )
12		eqidd	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( 2^nd ‘ 𝑃 ) = ( 2^nd ‘ 𝑃 ) )
13	7 8 9 10 11 12	prcofvalg	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( 𝑃 −∘_F 𝐹 ) = ⟨ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) , ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑙 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑎 ∈ ( 𝑘 ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1^st ‘ 𝐹 ) ) ) ) ⟩ )
14		ovex	⊢ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ∈ V
15	14	mptex	⊢ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) ∈ V
16	14 14	mpoex	⊢ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑙 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑎 ∈ ( 𝑘 ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1^st ‘ 𝐹 ) ) ) ) ∈ V
17	15 16	op1std	⊢ ( ( 𝑃 −∘_F 𝐹 ) = ⟨ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) , ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑙 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑎 ∈ ( 𝑘 ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1^st ‘ 𝐹 ) ) ) ) ⟩ → ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) = ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) )
18	13 17	syl	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) = ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) )
19	18	dmeqd	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) = dom ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) )
20	19	releqd	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( Rel dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) ↔ Rel dom ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) ) )
21	6 20	mpbiri	⊢ ( ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → Rel dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) )
22		rel0	⊢ Rel ∅
23		reldmprcof	⊢ Rel dom −∘_F
24	23	ovprc	⊢ ( ¬ ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( 𝑃 −∘_F 𝐹 ) = ∅ )
25	24	fveq2d	⊢ ( ¬ ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) = ( 1^st ‘ ∅ ) )
26		1st0	⊢ ( 1^st ‘ ∅ ) = ∅
27	25 26	eqtrdi	⊢ ( ¬ ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) = ∅ )
28	27	dmeqd	⊢ ( ¬ ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) = dom ∅ )
29		dm0	⊢ dom ∅ = ∅
30	28 29	eqtrdi	⊢ ( ¬ ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) = ∅ )
31	30	releqd	⊢ ( ¬ ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → ( Rel dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) ↔ Rel ∅ ) )
32	22 31	mpbiri	⊢ ( ¬ ( 𝑃 ∈ V ∧ 𝐹 ∈ V ) → Rel dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) ) )
33	21 32	pm2.61i	⊢ Rel dom ( 1^st ‘ ( 𝑃 −∘_F 𝐹 ) )

Metamath Proof Explorer

Theorem reldmprcof1

Proof