Metamath Proof Explorer

Theorem cicrcl

Description: Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020)

Ref Expression
Assertion cicrcl ⊢ C ∈ Cat ∧ R ≃ 𝑐 ⁡ C S → S ∈ Base C

Proof

Step Hyp Ref Expression
1 cicfval ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C = Iso ⁡ C supp ∅
2 1 breqd ⊢ C ∈ Cat → R ≃ 𝑐 ⁡ C S ↔ R supp ∅⁡ Iso ⁡ C S
3 isofn ⊢ C ∈ Cat → Iso ⁡ C Fn Base C × Base C
4 fvexd ⊢ C ∈ Cat → Iso ⁡ C ∈ V
5 0ex ⊢ ∅ ∈ V
6 5 a1i ⊢ C ∈ Cat → ∅ ∈ V
7 df-br ⊢ R supp ∅⁡ Iso ⁡ C S ↔ R S ∈ supp ∅⁡ Iso ⁡ C
8 elsuppfng ⊢ Iso ⁡ C Fn Base C × Base C ∧ Iso ⁡ C ∈ V ∧ ∅ ∈ V → R S ∈ supp ∅⁡ Iso ⁡ C ↔ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅
9 7 8 bitrid ⊢ Iso ⁡ C Fn Base C × Base C ∧ Iso ⁡ C ∈ V ∧ ∅ ∈ V → R supp ∅⁡ Iso ⁡ C S ↔ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅
10 3 4 6 9 syl3anc ⊢ C ∈ Cat → R supp ∅⁡ Iso ⁡ C S ↔ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅
11 opelxp2 ⊢ R S ∈ Base C × Base C → S ∈ Base C
12 11 adantr ⊢ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅ → S ∈ Base C
13 10 12 biimtrdi ⊢ C ∈ Cat → R supp ∅⁡ Iso ⁡ C S → S ∈ Base C
14 2 13 sylbid ⊢ C ∈ Cat → R ≃ 𝑐 ⁡ C S → S ∈ Base C
15 14 imp ⊢ C ∈ Cat ∧ R ≃ 𝑐 ⁡ C S → S ∈ Base C