Metamath Proof Explorer

Theorem uobrcl

Description: Reverse closure for universal object. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Assertion uobrcl ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )

Proof

Step Hyp Ref Expression
1 eldmg ⊢ ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) → ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ↔ ∃ 𝑚 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑚 ) )
2 1 ibi ⊢ ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) → ∃ 𝑚 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑚 )
3 simpr ⊢ ( ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ∧ 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑚 ) → 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑚 )
4 3 up1st2nd ⊢ ( ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ∧ 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑚 ) → 𝑋 ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑚 )
5 4 uprcl2 ⊢ ( ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ∧ 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑚 ) → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
6 2 5 exlimddv ⊢ ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
7 6 funcrcl2 ⊢ ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) → 𝐷 ∈ Cat )
8 6 funcrcl3 ⊢ ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) → 𝐸 ∈ Cat )
9 7 8 jca ⊢ ( 𝑋 ∈ dom ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )