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

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝑃 ∈ ( ≃𝑐 ‘ 𝐷 ) )