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

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 bitrid ⊢ ( ( ( 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 biimtrdi ⊢ ( 𝐶 ∈ Cat → ( 𝑅 ( ( Iso ‘ 𝐶 ) supp ∅ ) 𝑆 → 𝑆 ∈ ( Base ‘ 𝐶 ) ) )
14 2 13 sylbid ⊢ ( 𝐶 ∈ Cat → ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 → 𝑆 ∈ ( Base ‘ 𝐶 ) ) )
15 14 imp ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )