Theorem cicpropdlem

Description: Lemma for cicpropd . (Contributed by Zhi Wang, 27-Oct-2025)

	Ref	Expression
Hypotheses	cicpropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
	cicpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
Assertion	cicpropdlem	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝑃 ∈ ( ≃𝑐 ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		cicpropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2		cicpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3		cic1st2nd	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
5		cic1st2ndbr	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) )
6	5	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
9	7 8	isopropd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐷 ) )
10	9	oveqd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( ( 1st ‘ 𝑃 ) ( Iso ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) ) = ( ( 1st ‘ 𝑃 ) ( Iso ‘ 𝐷 ) ( 2nd ‘ 𝑃 ) ) )
11	10	neeq1d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( ( ( 1st ‘ 𝑃 ) ( Iso ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) ) ≠ ∅ ↔ ( ( 1st ‘ 𝑃 ) ( Iso ‘ 𝐷 ) ( 2nd ‘ 𝑃 ) ) ≠ ∅ ) )
12		eqid	⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
13		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14		cicrcl2	⊢ ( ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) → 𝐶 ∈ Cat )
15	5 14	syl	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝐶 ∈ Cat )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
17		ciclcl	⊢ ( ( 𝐶 ∈ Cat ∧ ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) ) → ( 1st ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
18	14 17	mpancom	⊢ ( ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) → ( 1st ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
19	5 18	syl	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → ( 1st ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( 1st ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
21		cicrcl	⊢ ( ( 𝐶 ∈ Cat ∧ ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) ) → ( 2nd ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
22	14 21	mpancom	⊢ ( ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) → ( 2nd ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
23	5 22	syl	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → ( 2nd ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( 2nd ‘ 𝑃 ) ∈ ( Base ‘ 𝐶 ) )
25	12 13 16 20 24	brcic	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) ↔ ( ( 1st ‘ 𝑃 ) ( Iso ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) ) ≠ ∅ ) )
26		eqid	⊢ ( Iso ‘ 𝐷 ) = ( Iso ‘ 𝐷 )
27		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
28	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
30	20 29	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( 1st ‘ 𝑃 ) ∈ ( Base ‘ 𝐷 ) )
31	30	elfvexd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝐷 ∈ V )
32	7 8 16 31	catpropd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
33	16 32	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
34	24 29	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( 2nd ‘ 𝑃 ) ∈ ( Base ‘ 𝐷 ) )
35	26 27 33 30 34	brcic	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐷 ) ( 2nd ‘ 𝑃 ) ↔ ( ( 1st ‘ 𝑃 ) ( Iso ‘ 𝐷 ) ( 2nd ‘ 𝑃 ) ) ≠ ∅ ) )
36	11 25 35	3bitr4d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑃 ) ↔ ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐷 ) ( 2nd ‘ 𝑃 ) ) )
37	6 36	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐷 ) ( 2nd ‘ 𝑃 ) )
38		df-br	⊢ ( ( 1st ‘ 𝑃 ) ( ≃𝑐 ‘ 𝐷 ) ( 2nd ‘ 𝑃 ) ↔ ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( ≃𝑐 ‘ 𝐷 ) )
39	37 38	sylib	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( ≃𝑐 ‘ 𝐷 ) )
40	4 39	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝑃 ∈ ( ≃𝑐 ‘ 𝐷 ) )