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 ‘ 𝐶 ) )