Metamath Proof Explorer

Theorem rngcisoALTV

Description: An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses rngcsectALTV.c ⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
rngcsectALTV.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
rngcsectALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcsectALTV.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rngcsectALTV.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
rngcisoALTV.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion rngcisoALTV ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 rngcsectALTV.c ⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
2 rngcsectALTV.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 rngcsectALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 rngcsectALTV.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 rngcsectALTV.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 rngcisoALTV.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
7 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
8 1 rngccatALTV ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
9 3 8 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 2 7 9 4 5 6 isoval ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
11 10 eleq2d ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
12 2 7 9 4 5 invfun ⊢ ( 𝜑 → Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
13 funfvbrb ⊢ ( Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
14 12 13 syl ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
15 1 2 3 4 5 7 rngcinvALTV ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) = ◡ 𝐹 ) ) )
16 simpl ⊢ ( ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) = ◡ 𝐹 ) → 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) )
17 15 16 syl6bi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) → 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ) )
18 14 17 sylbid ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ) )
19 eqid ⊢ ◡ 𝐹 = ◡ 𝐹
20 1 2 3 4 5 7 rngcinvALTV ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 ↔ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ ◡ 𝐹 = ◡ 𝐹 ) ) )
21 funrel ⊢ ( Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
22 12 21 syl ⊢ ( 𝜑 → Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
23 releldm ⊢ ( ( Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
24 23 ex ⊢ ( Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
25 22 24 syl ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
26 20 25 sylbird ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ ◡ 𝐹 = ◡ 𝐹 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
27 19 26 mpan2i ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
28 18 27 impbid ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ) )
29 11 28 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ) )