This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isoval2

Description: The isomorphisms are the domain of the inverse relation. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses isoval2.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
isoval2.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion isoval2 ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 )

Proof

Step Hyp Ref Expression
1 isoval2.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
2 isoval2.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
3 id ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 2 3 isorcl ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝐶 ∈ Cat )
6 2 3 4 isorcl2 ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
7 6 simpld ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
8 6 simprd ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
9 4 1 5 7 8 2 isoval ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 ) )
10 3 9 eleqtrd ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) )
11 vex ⊢ 𝑓 ∈ V
12 11 eldm ⊢ ( 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) ↔ ∃ 𝑔 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 )
13 id ⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 )
14 1 13 invrcl ⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝐶 ∈ Cat )
15 1 13 4 invrcl2 ⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
16 15 simpld ⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
17 15 simprd ⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
18 4 1 14 16 17 2 13 inviso1 ⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
19 18 exlimiv ⊢ ( ∃ 𝑔 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
20 12 19 sylbi ⊢ ( 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
21 10 20 impbii ⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) )
22 21 eqriv ⊢ ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 )