isopropdlem

	Ref	Expression
Hypotheses	sectpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	sectpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
Assertion	isopropdlem	$⊢ (φ \land P \in Iso (C)) \to P \in Iso (D)$

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		sectpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3		simpr	$⊢ (φ \land P \in Iso (C)) \to P \in Iso (C)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqid	$⊢ Inv (C) = Inv (C)$
6		df-iso	$⊢ Iso = (c \in Cat ⟼ (x \in V ⟼ dom x) \circ Inv (c))$
7	6	mptrcl	$⊢ P \in Iso (C) \to C \in Cat$
8	7	adantl	$⊢ (φ \land P \in Iso (C)) \to C \in Cat$
9		eqid	$⊢ Iso (C) = Iso (C)$
10	4 5 8 9	isofval2	$⊢ (φ \land P \in Iso (C)) \to Iso (C) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ dom (x Inv (C) y))$
11		df-mpo	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ dom (x Inv (C) y)) = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (x Inv (C) y))\}$
12	10 11	eqtrdi	$⊢ (φ \land P \in Iso (C)) \to Iso (C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (x Inv (C) y))\}$
13	3 12	eleqtrd	$⊢ (φ \land P \in Iso (C)) \to P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (x Inv (C) y))\}$
14		eloprab1st2nd	$⊢ P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (x Inv (C) y))\} \to P = ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩$
15	13 14	syl	$⊢ (φ \land P \in Iso (C)) \to P = ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩$
16	1	adantr	$⊢ (φ \land P \in Iso (C)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
17	2	adantr	$⊢ (φ \land P \in Iso (C)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
18	16 17	invpropd	$⊢ (φ \land P \in Iso (C)) \to Inv (C) = Inv (D)$
19	18	oveqd	$⊢ (φ \land P \in Iso (C)) \to 1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P)) = 1^{st} (1^{st} (P)) Inv (D) 2^{nd} (1^{st} (P))$
20	19	dmeqd	$⊢ (φ \land P \in Iso (C)) \to dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P))) = dom (1^{st} (1^{st} (P)) Inv (D) 2^{nd} (1^{st} (P)))$
21		eleq1	$⊢ x = 1^{st} (1^{st} (P)) \to (x \in {Base}_{C} \leftrightarrow 1^{st} (1^{st} (P)) \in {Base}_{C})$
22	21	anbi1d	$⊢ x = 1^{st} (1^{st} (P)) \to ((x \in {Base}_{C} \land y \in {Base}_{C}) \leftrightarrow (1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}))$
23		oveq1	$⊢ x = 1^{st} (1^{st} (P)) \to x Inv (C) y = 1^{st} (1^{st} (P)) Inv (C) y$
24	23	dmeqd	$⊢ x = 1^{st} (1^{st} (P)) \to dom (x Inv (C) y) = dom (1^{st} (1^{st} (P)) Inv (C) y)$
25	24	eqeq2d	$⊢ x = 1^{st} (1^{st} (P)) \to (z = dom (x Inv (C) y) \leftrightarrow z = dom (1^{st} (1^{st} (P)) Inv (C) y))$
26	22 25	anbi12d	$⊢ x = 1^{st} (1^{st} (P)) \to (((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (x Inv (C) y)) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (1^{st} (1^{st} (P)) Inv (C) y)))$
27		eleq1	$⊢ y = 2^{nd} (1^{st} (P)) \to (y \in {Base}_{C} \leftrightarrow 2^{nd} (1^{st} (P)) \in {Base}_{C})$
28	27	anbi2d	$⊢ y = 2^{nd} (1^{st} (P)) \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \leftrightarrow (1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}))$
29		oveq2	$⊢ y = 2^{nd} (1^{st} (P)) \to 1^{st} (1^{st} (P)) Inv (C) y = 1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P))$
30	29	dmeqd	$⊢ y = 2^{nd} (1^{st} (P)) \to dom (1^{st} (1^{st} (P)) Inv (C) y) = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P)))$
31	30	eqeq2d	$⊢ y = 2^{nd} (1^{st} (P)) \to (z = dom (1^{st} (1^{st} (P)) Inv (C) y) \leftrightarrow z = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P))))$
32	28 31	anbi12d	$⊢ y = 2^{nd} (1^{st} (P)) \to (((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (1^{st} (1^{st} (P)) Inv (C) y)) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land z = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P)))))$
33		eqeq1	$⊢ z = 2^{nd} (P) \to (z = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P))) \leftrightarrow 2^{nd} (P) = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P))))$
34	33	anbi2d	$⊢ z = 2^{nd} (P) \to (((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land z = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P)))) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P)))))$
35	26 32 34	eloprabi	$⊢ P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = dom (x Inv (C) y))\} \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P))))$
36	13 35	syl	$⊢ (φ \land P \in Iso (C)) \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P))))$
37	36	simprd	$⊢ (φ \land P \in Iso (C)) \to 2^{nd} (P) = dom (1^{st} (1^{st} (P)) Inv (C) 2^{nd} (1^{st} (P)))$
38		eqid	$⊢ {Base}_{D} = {Base}_{D}$
39		eqid	$⊢ Inv (D) = Inv (D)$
40	36	simplld	$⊢ (φ \land P \in Iso (C)) \to 1^{st} (1^{st} (P)) \in {Base}_{C}$
41	16	homfeqbas	$⊢ (φ \land P \in Iso (C)) \to {Base}_{C} = {Base}_{D}$
42	40 41	eleqtrd	$⊢ (φ \land P \in Iso (C)) \to 1^{st} (1^{st} (P)) \in {Base}_{D}$
43	42	elfvexd	$⊢ (φ \land P \in Iso (C)) \to D \in V$
44	16 17 8 43	catpropd	$⊢ (φ \land P \in Iso (C)) \to (C \in Cat \leftrightarrow D \in Cat)$
45	8 44	mpbid	$⊢ (φ \land P \in Iso (C)) \to D \in Cat$
46	36	simplrd	$⊢ (φ \land P \in Iso (C)) \to 2^{nd} (1^{st} (P)) \in {Base}_{C}$
47	46 41	eleqtrd	$⊢ (φ \land P \in Iso (C)) \to 2^{nd} (1^{st} (P)) \in {Base}_{D}$
48		eqid	$⊢ Iso (D) = Iso (D)$
49	38 39 45 42 47 48	isoval	$⊢ (φ \land P \in Iso (C)) \to 1^{st} (1^{st} (P)) Iso (D) 2^{nd} (1^{st} (P)) = dom (1^{st} (1^{st} (P)) Inv (D) 2^{nd} (1^{st} (P)))$
50	20 37 49	3eqtr4rd	$⊢ (φ \land P \in Iso (C)) \to 1^{st} (1^{st} (P)) Iso (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P)$
51		isofn	$⊢ D \in Cat \to Iso (D) Fn ({Base}_{D} \times {Base}_{D})$
52	45 51	syl	$⊢ (φ \land P \in Iso (C)) \to Iso (D) Fn ({Base}_{D} \times {Base}_{D})$
53		fnbrovb	$⊢ (Iso (D) Fn ({Base}_{D} \times {Base}_{D}) \land (1^{st} (1^{st} (P)) \in {Base}_{D} \land 2^{nd} (1^{st} (P)) \in {Base}_{D})) \to (1^{st} (1^{st} (P)) Iso (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P) \leftrightarrow ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Iso (D) 2^{nd} (P))$
54	52 42 47 53	syl12anc	$⊢ (φ \land P \in Iso (C)) \to (1^{st} (1^{st} (P)) Iso (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P) \leftrightarrow ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Iso (D) 2^{nd} (P))$
55	50 54	mpbid	$⊢ (φ \land P \in Iso (C)) \to ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Iso (D) 2^{nd} (P)$
56		df-br	$⊢ ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Iso (D) 2^{nd} (P) \leftrightarrow ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩ \in Iso (D)$
57	55 56	sylib	$⊢ (φ \land P \in Iso (C)) \to ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩ \in Iso (D)$
58	15 57	eqeltrd	$⊢ (φ \land P \in Iso (C)) \to P \in Iso (D)$

Metamath Proof Explorer

Theorem isopropdlem

Proof