reldmran2

Description: The domain of ( P Ran E ) is a relation. (Contributed by Zhi Wang, 4-Nov-2025)

		Ref	Expression
	Assertion	reldmran2	⊢ Rel dom ( 𝑃 Ran 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		rel0	⊢ Rel ∅
2		df-ov	⊢ ( 𝑃 Ran 𝐸 ) = ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ )
3		id	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) = ∅ → ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) = ∅ )
4	2 3	eqtrid	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) = ∅ → ( 𝑃 Ran 𝐸 ) = ∅ )
5	4	dmeqd	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) = ∅ → dom ( 𝑃 Ran 𝐸 ) = dom ∅ )
6		dm0	⊢ dom ∅ = ∅
7	5 6	eqtrdi	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) = ∅ → dom ( 𝑃 Ran 𝐸 ) = ∅ )
8	7	releqd	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) = ∅ → ( Rel dom ( 𝑃 Ran 𝐸 ) ↔ Rel ∅ ) )
9	1 8	mpbiri	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) = ∅ → Rel dom ( 𝑃 Ran 𝐸 ) )
10		eqid	⊢ ( 𝑓 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑥 ∈ ( ( 1^st ‘ 𝑃 ) Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ ( 2^nd ‘ 𝑃 ) , 𝐸 ⟩ −∘_F 𝑓 ) ) ( ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) UP ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) ) 𝑥 ) ) = ( 𝑓 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑥 ∈ ( ( 1^st ‘ 𝑃 ) Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ ( 2^nd ‘ 𝑃 ) , 𝐸 ⟩ −∘_F 𝑓 ) ) ( ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) UP ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) ) 𝑥 ) )
11	10	reldmmpo	⊢ Rel dom ( 𝑓 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑥 ∈ ( ( 1^st ‘ 𝑃 ) Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ ( 2^nd ‘ 𝑃 ) , 𝐸 ⟩ −∘_F 𝑓 ) ) ( ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) UP ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) ) 𝑥 ) )
12		fvfundmfvn0	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ( ⟨ 𝑃 , 𝐸 ⟩ ∈ dom Ran ∧ Fun ( Ran ↾ { ⟨ 𝑃 , 𝐸 ⟩ } ) ) )
13	12	simpld	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ⟨ 𝑃 , 𝐸 ⟩ ∈ dom Ran )
14		ranfn	⊢ Ran Fn ( ( V × V ) × V )
15	14	fndmi	⊢ dom Ran = ( ( V × V ) × V )
16	13 15	eleqtrdi	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ⟨ 𝑃 , 𝐸 ⟩ ∈ ( ( V × V ) × V ) )
17		opelxp1	⊢ ( ⟨ 𝑃 , 𝐸 ⟩ ∈ ( ( V × V ) × V ) → 𝑃 ∈ ( V × V ) )
18		1st2nd2	⊢ ( 𝑃 ∈ ( V × V ) → 𝑃 = ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ )
19	16 17 18	3syl	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → 𝑃 = ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ )
20	19	oveq1d	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ( 𝑃 Ran 𝐸 ) = ( ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ Ran 𝐸 ) )
21		eqid	⊢ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) = ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 )
22		eqid	⊢ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) = ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 )
23		fvexd	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ( 1^st ‘ 𝑃 ) ∈ V )
24		fvexd	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ( 2^nd ‘ 𝑃 ) ∈ V )
25		opelxp2	⊢ ( ⟨ 𝑃 , 𝐸 ⟩ ∈ ( ( V × V ) × V ) → 𝐸 ∈ V )
26	16 25	syl	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → 𝐸 ∈ V )
27		eqid	⊢ ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) = ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) )
28		eqid	⊢ ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) = ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) )
29	21 22 23 24 26 27 28	ranfval	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ( ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ Ran 𝐸 ) = ( 𝑓 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑥 ∈ ( ( 1^st ‘ 𝑃 ) Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ ( 2^nd ‘ 𝑃 ) , 𝐸 ⟩ −∘_F 𝑓 ) ) ( ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) UP ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) ) 𝑥 ) ) )
30	20 29	eqtrd	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ( 𝑃 Ran 𝐸 ) = ( 𝑓 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑥 ∈ ( ( 1^st ‘ 𝑃 ) Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ ( 2^nd ‘ 𝑃 ) , 𝐸 ⟩ −∘_F 𝑓 ) ) ( ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) UP ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) ) 𝑥 ) ) )
31	30	dmeqd	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → dom ( 𝑃 Ran 𝐸 ) = dom ( 𝑓 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑥 ∈ ( ( 1^st ‘ 𝑃 ) Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ ( 2^nd ‘ 𝑃 ) , 𝐸 ⟩ −∘_F 𝑓 ) ) ( ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) UP ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) ) 𝑥 ) ) )
32	31	releqd	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → ( Rel dom ( 𝑃 Ran 𝐸 ) ↔ Rel dom ( 𝑓 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑥 ∈ ( ( 1^st ‘ 𝑃 ) Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ ( 2^nd ‘ 𝑃 ) , 𝐸 ⟩ −∘_F 𝑓 ) ) ( ( oppCat ‘ ( ( 2^nd ‘ 𝑃 ) FuncCat 𝐸 ) ) UP ( oppCat ‘ ( ( 1^st ‘ 𝑃 ) FuncCat 𝐸 ) ) ) 𝑥 ) ) ) )
33	11 32	mpbiri	⊢ ( ( Ran ‘ ⟨ 𝑃 , 𝐸 ⟩ ) ≠ ∅ → Rel dom ( 𝑃 Ran 𝐸 ) )
34	9 33	pm2.61ine	⊢ Rel dom ( 𝑃 Ran 𝐸 )

Metamath Proof Explorer

Theorem reldmran2

Proof