Metamath Proof Explorer


Theorem cicrcl

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

Ref Expression
Assertion cicrcl ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐𝐶 ) 𝑆 ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cicfval ( 𝐶 ∈ Cat → ( ≃𝑐𝐶 ) = ( ( Iso ‘ 𝐶 ) supp ∅ ) )
2 1 breqd ( 𝐶 ∈ Cat → ( 𝑅 ( ≃𝑐𝐶 ) 𝑆𝑅 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑆 ) )
3 isofn ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
4 fvexd ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) ∈ V )
5 0ex ∅ ∈ V
6 5 a1i ( 𝐶 ∈ Cat → ∅ ∈ V )
7 df-br ( 𝑅 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑆 ↔ ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( Iso ‘ 𝐶 ) supp ∅ ) )
8 elsuppfng ( ( ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( Iso ‘ 𝐶 ) ∈ V ∧ ∅ ∈ V ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( Iso ‘ 𝐶 ) supp ∅ ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ≠ ∅ ) ) )
9 7 8 syl5bb ( ( ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( Iso ‘ 𝐶 ) ∈ V ∧ ∅ ∈ V ) → ( 𝑅 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑆 ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ≠ ∅ ) ) )
10 3 4 6 9 syl3anc ( 𝐶 ∈ Cat → ( 𝑅 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑆 ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ≠ ∅ ) ) )
11 opelxp2 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
12 11 adantr ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ≠ ∅ ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
13 10 12 syl6bi ( 𝐶 ∈ Cat → ( 𝑅 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑆𝑆 ∈ ( Base ‘ 𝐶 ) ) )
14 2 13 sylbid ( 𝐶 ∈ Cat → ( 𝑅 ( ≃𝑐𝐶 ) 𝑆𝑆 ∈ ( Base ‘ 𝐶 ) ) )
15 14 imp ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐𝐶 ) 𝑆 ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )