cicpropdlem

	Ref	Expression
Hypotheses	cicpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	cicpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
Assertion	cicpropdlem	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to P \in ≃_{𝑐} (D)$

Proof

Step	Hyp	Ref	Expression
1		cicpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		cicpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3		cic1st2nd	$⊢ P \in ≃_{𝑐} (C) \to P = ⟨1^{st} (P), 2^{nd} (P)⟩$
4	3	adantl	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to P = ⟨1^{st} (P), 2^{nd} (P)⟩$
5		cic1st2ndbr	$⊢ P \in ≃_{𝑐} (C) \to 1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P)$
6	5	adantl	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to 1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P)$
7	1	adantr	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
8	2	adantr	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
9	7 8	isopropd	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to Iso (C) = Iso (D)$
10	9	oveqd	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to 1^{st} (P) Iso (C) 2^{nd} (P) = 1^{st} (P) Iso (D) 2^{nd} (P)$
11	10	neeq1d	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to (1^{st} (P) Iso (C) 2^{nd} (P) \neq \emptyset \leftrightarrow 1^{st} (P) Iso (D) 2^{nd} (P) \neq \emptyset)$
12		eqid	$⊢ Iso (C) = Iso (C)$
13		eqid	$⊢ {Base}_{C} = {Base}_{C}$
14		cicrcl2	$⊢ 1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P) \to C \in Cat$
15	5 14	syl	$⊢ P \in ≃_{𝑐} (C) \to C \in Cat$
16	15	adantl	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to C \in Cat$
17		ciclcl	$⊢ (C \in Cat \land 1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P)) \to 1^{st} (P) \in {Base}_{C}$
18	14 17	mpancom	$⊢ 1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P) \to 1^{st} (P) \in {Base}_{C}$
19	5 18	syl	$⊢ P \in ≃_{𝑐} (C) \to 1^{st} (P) \in {Base}_{C}$
20	19	adantl	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to 1^{st} (P) \in {Base}_{C}$
21		cicrcl	$⊢ (C \in Cat \land 1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P)) \to 2^{nd} (P) \in {Base}_{C}$
22	14 21	mpancom	$⊢ 1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P) \to 2^{nd} (P) \in {Base}_{C}$
23	5 22	syl	$⊢ P \in ≃_{𝑐} (C) \to 2^{nd} (P) \in {Base}_{C}$
24	23	adantl	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to 2^{nd} (P) \in {Base}_{C}$
25	12 13 16 20 24	brcic	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to (1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P) \leftrightarrow 1^{st} (P) Iso (C) 2^{nd} (P) \neq \emptyset)$
26		eqid	$⊢ Iso (D) = Iso (D)$
27		eqid	$⊢ {Base}_{D} = {Base}_{D}$
28	1	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
29	28	adantr	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to {Base}_{C} = {Base}_{D}$
30	20 29	eleqtrd	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to 1^{st} (P) \in {Base}_{D}$
31	30	elfvexd	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to D \in V$
32	7 8 16 31	catpropd	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to (C \in Cat \leftrightarrow D \in Cat)$
33	16 32	mpbid	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to D \in Cat$
34	24 29	eleqtrd	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to 2^{nd} (P) \in {Base}_{D}$
35	26 27 33 30 34	brcic	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to (1^{st} (P) ≃_{𝑐} (D) 2^{nd} (P) \leftrightarrow 1^{st} (P) Iso (D) 2^{nd} (P) \neq \emptyset)$
36	11 25 35	3bitr4d	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to (1^{st} (P) ≃_{𝑐} (C) 2^{nd} (P) \leftrightarrow 1^{st} (P) ≃_{𝑐} (D) 2^{nd} (P))$
37	6 36	mpbid	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to 1^{st} (P) ≃_{𝑐} (D) 2^{nd} (P)$
38		df-br	$⊢ 1^{st} (P) ≃_{𝑐} (D) 2^{nd} (P) \leftrightarrow ⟨1^{st} (P), 2^{nd} (P)⟩ \in ≃_{𝑐} (D)$
39	37 38	sylib	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to ⟨1^{st} (P), 2^{nd} (P)⟩ \in ≃_{𝑐} (D)$
40	4 39	eqeltrd	$⊢ (φ \land P \in ≃_{𝑐} (C)) \to P \in ≃_{𝑐} (D)$

Metamath Proof Explorer

Theorem cicpropdlem

Proof