Metamath Proof Explorer

Theorem brcic

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

Ref Expression
Hypotheses cic.i ⊢ I = Iso ⁡ C
cic.b ⊢ B = Base C
cic.c ⊢ φ → C ∈ Cat
cic.x ⊢ φ → X ∈ B
cic.y ⊢ φ → Y ∈ B
Assertion brcic ⊢ φ → X ≃ 𝑐 ⁡ C Y ↔ X I Y ≠ ∅

Proof

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