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

Metamath Proof Explorer

Theorem brcic

Description: The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020)

Ref Expression
Hypotheses cic.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
cic.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
cic.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
cic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
cic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion brcic ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ( 𝑋 𝐼 𝑌 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 cic.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
2 cic.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 cic.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 cic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 cic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 cicfval ⊢ ( 𝐶 ∈ Cat → ( ≃𝑐 ‘ 𝐶 ) = ( ( Iso ‘ 𝐶 ) supp ∅ ) )
7 3 6 syl ⊢ ( 𝜑 → ( ≃𝑐 ‘ 𝐶 ) = ( ( Iso ‘ 𝐶 ) supp ∅ ) )
8 7 breqd ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ 𝑋 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑌 ) )
9 df-br ⊢ ( 𝑋 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Iso ‘ 𝐶 ) supp ∅ ) )
10 9 a1i ⊢ ( 𝜑 → ( 𝑋 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Iso ‘ 𝐶 ) supp ∅ ) ) )
11 1 a1i ⊢ ( 𝜑 → 𝐼 = ( Iso ‘ 𝐶 ) )
12 11 fveq1d ⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
13 12 neeq1d ⊢ ( 𝜑 → ( ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ≠ ∅ ↔ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ≠ ∅ ) )
14 df-ov ⊢ ( 𝑋 𝐼 𝑌 ) = ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
15 14 eqcomi ⊢ ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑋 𝐼 𝑌 )
16 15 a1i ⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑋 𝐼 𝑌 ) )
17 16 neeq1d ⊢ ( 𝜑 → ( ( 𝐼 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ≠ ∅ ↔ ( 𝑋 𝐼 𝑌 ) ≠ ∅ ) )
18 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) ∈ V )
19 18 18 xpexd ⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V )
20 4 2 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
21 5 2 eleqtrdi ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
22 20 21 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
23 isofn ⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
24 3 23 syl ⊢ ( 𝜑 → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
25 fvn0elsuppb ⊢ ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ≠ ∅ ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Iso ‘ 𝐶 ) supp ∅ ) ) )
26 19 22 24 25 syl3anc ⊢ ( 𝜑 → ( ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ≠ ∅ ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Iso ‘ 𝐶 ) supp ∅ ) ) )
27 13 17 26 3bitr3rd ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Iso ‘ 𝐶 ) supp ∅ ) ↔ ( 𝑋 𝐼 𝑌 ) ≠ ∅ ) )
28 8 10 27 3bitrd ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ( 𝑋 𝐼 𝑌 ) ≠ ∅ ) )