reldmlan2

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

		Ref	Expression
	Assertion	reldmlan2	⊢ Rel dom ( 𝑃 Lan 𝐸 )

Proof

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

Metamath Proof Explorer

Theorem reldmlan2

Proof