reldmprcof2

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

		Ref	Expression
	Assertion	reldmprcof2	⊢ Rel dom ( 2^nd ‘ ( 𝑃 −∘_F 𝐹 ) )

Proof

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

Metamath Proof Explorer

Theorem reldmprcof2

Proof