Metamath Proof Explorer

Theorem ciclcl

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

Ref Expression
Assertion ciclcl ⊢ C ∈ Cat ∧ R ≃ 𝑐 ⁡ C S → R ∈ 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 fvex ⊢ Base C ∈ V
5 sqxpexg ⊢ Base C ∈ V → Base C × Base C ∈ V
6 4 5 mp1i ⊢ C ∈ Cat → Base C × Base C ∈ V
7 0ex ⊢ ∅ ∈ V
8 7 a1i ⊢ C ∈ Cat → ∅ ∈ V
9 df-br ⊢ R supp ∅⁡ Iso ⁡ C S ↔ R S ∈ supp ∅⁡ Iso ⁡ C
10 elsuppfn ⊢ Iso ⁡ C Fn Base C × Base C ∧ Base C × Base C ∈ V ∧ ∅ ∈ V → R S ∈ supp ∅⁡ Iso ⁡ C ↔ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅
11 9 10 syl5bb ⊢ Iso ⁡ C Fn Base C × Base C ∧ Base C × Base C ∈ V ∧ ∅ ∈ V → R supp ∅⁡ Iso ⁡ C S ↔ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅
12 3 6 8 11 syl3anc ⊢ C ∈ Cat → R supp ∅⁡ Iso ⁡ C S ↔ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅
13 opelxp1 ⊢ R S ∈ Base C × Base C → R ∈ Base C
14 13 adantr ⊢ R S ∈ Base C × Base C ∧ Iso ⁡ C ⁡ R S ≠ ∅ → R ∈ Base C
15 12 14 syl6bi ⊢ C ∈ Cat → R supp ∅⁡ Iso ⁡ C S → R ∈ Base C
16 2 15 sylbid ⊢ C ∈ Cat → R ≃ 𝑐 ⁡ C S → R ∈ Base C
17 16 imp ⊢ C ∈ Cat ∧ R ≃ 𝑐 ⁡ C S → R ∈ Base C