invpropdlem

	Ref	Expression
Hypotheses	sectpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	sectpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
Assertion	invpropdlem	$⊢ (φ \land P \in Inv (C)) \to P \in Inv (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 Inv (C)) \to P \in Inv (C)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqid	$⊢ Inv (C) = Inv (C)$
6		df-inv	$⊢ Inv = (c \in Cat ⟼ (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (x Sect (c) y) \cap {(y Sect (c) x)}^{-1}))$
7	6	mptrcl	$⊢ P \in Inv (C) \to C \in Cat$
8	7	adantl	$⊢ (φ \land P \in Inv (C)) \to C \in Cat$
9		eqid	$⊢ Sect (C) = Sect (C)$
10	4 5 8 9	invffval	$⊢ (φ \land P \in Inv (C)) \to Inv (C) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})$
11		df-mpo	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1}) = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})\}$
12	10 11	eqtrdi	$⊢ (φ \land P \in Inv (C)) \to Inv (C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})\}$
13	3 12	eleqtrd	$⊢ (φ \land P \in Inv (C)) \to P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})\}$
14		eloprab1st2nd	$⊢ P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})\} \to P = ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩$
15	13 14	syl	$⊢ (φ \land P \in Inv (C)) \to P = ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩$
16	1	adantr	$⊢ (φ \land P \in Inv (C)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
17	2	adantr	$⊢ (φ \land P \in Inv (C)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
18	16 17	sectpropd	$⊢ (φ \land P \in Inv (C)) \to Sect (C) = Sect (D)$
19	18	oveqd	$⊢ (φ \land P \in Inv (C)) \to 1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P)) = 1^{st} (1^{st} (P)) Sect (D) 2^{nd} (1^{st} (P))$
20	18	oveqd	$⊢ (φ \land P \in Inv (C)) \to 2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)) = 2^{nd} (1^{st} (P)) Sect (D) 1^{st} (1^{st} (P))$
21	20	cnveqd	$⊢ (φ \land P \in Inv (C)) \to {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1} = {(2^{nd} (1^{st} (P)) Sect (D) 1^{st} (1^{st} (P)))}^{-1}$
22	19 21	ineq12d	$⊢ (φ \land P \in Inv (C)) \to (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1} = (1^{st} (1^{st} (P)) Sect (D) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (D) 1^{st} (1^{st} (P)))}^{-1}$
23		eleq1	$⊢ x = 1^{st} (1^{st} (P)) \to (x \in {Base}_{C} \leftrightarrow 1^{st} (1^{st} (P)) \in {Base}_{C})$
24	23	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}))$
25		oveq1	$⊢ x = 1^{st} (1^{st} (P)) \to x Sect (C) y = 1^{st} (1^{st} (P)) Sect (C) y$
26		oveq2	$⊢ x = 1^{st} (1^{st} (P)) \to y Sect (C) x = y Sect (C) 1^{st} (1^{st} (P))$
27	26	cnveqd	$⊢ x = 1^{st} (1^{st} (P)) \to {(y Sect (C) x)}^{-1} = {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1}$
28	25 27	ineq12d	$⊢ x = 1^{st} (1^{st} (P)) \to (x Sect (C) y) \cap {(y Sect (C) x)}^{-1} = (1^{st} (1^{st} (P)) Sect (C) y) \cap {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1}$
29	28	eqeq2d	$⊢ x = 1^{st} (1^{st} (P)) \to (z = (x Sect (C) y) \cap {(y Sect (C) x)}^{-1} \leftrightarrow z = (1^{st} (1^{st} (P)) Sect (C) y) \cap {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1})$
30	24 29	anbi12d	$⊢ x = 1^{st} (1^{st} (P)) \to (((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = (x Sect (C) y) \cap {(y Sect (C) x)}^{-1}) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \land z = (1^{st} (1^{st} (P)) Sect (C) y) \cap {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1}))$
31		eleq1	$⊢ y = 2^{nd} (1^{st} (P)) \to (y \in {Base}_{C} \leftrightarrow 2^{nd} (1^{st} (P)) \in {Base}_{C})$
32	31	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}))$
33		oveq2	$⊢ y = 2^{nd} (1^{st} (P)) \to 1^{st} (1^{st} (P)) Sect (C) y = 1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))$
34		oveq1	$⊢ y = 2^{nd} (1^{st} (P)) \to y Sect (C) 1^{st} (1^{st} (P)) = 2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P))$
35	34	cnveqd	$⊢ y = 2^{nd} (1^{st} (P)) \to {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1} = {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1}$
36	33 35	ineq12d	$⊢ y = 2^{nd} (1^{st} (P)) \to (1^{st} (1^{st} (P)) Sect (C) y) \cap {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1} = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1}$
37	36	eqeq2d	$⊢ y = 2^{nd} (1^{st} (P)) \to (z = (1^{st} (1^{st} (P)) Sect (C) y) \cap {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1} \leftrightarrow z = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1})$
38	32 37	anbi12d	$⊢ y = 2^{nd} (1^{st} (P)) \to (((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \land z = (1^{st} (1^{st} (P)) Sect (C) y) \cap {(y Sect (C) 1^{st} (1^{st} (P)))}^{-1}) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land z = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1}))$
39		eqeq1	$⊢ z = 2^{nd} (P) \to (z = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1} \leftrightarrow 2^{nd} (P) = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1})$
40	39	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 = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1}) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1}))$
41	30 38 40	eloprabi	$⊢ P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})\} \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1})$
42	13 41	syl	$⊢ (φ \land P \in Inv (C)) \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1})$
43	42	simprd	$⊢ (φ \land P \in Inv (C)) \to 2^{nd} (P) = (1^{st} (1^{st} (P)) Sect (C) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (C) 1^{st} (1^{st} (P)))}^{-1}$
44		eqid	$⊢ {Base}_{D} = {Base}_{D}$
45		eqid	$⊢ Inv (D) = Inv (D)$
46	42	simplld	$⊢ (φ \land P \in Inv (C)) \to 1^{st} (1^{st} (P)) \in {Base}_{C}$
47	16	homfeqbas	$⊢ (φ \land P \in Inv (C)) \to {Base}_{C} = {Base}_{D}$
48	46 47	eleqtrd	$⊢ (φ \land P \in Inv (C)) \to 1^{st} (1^{st} (P)) \in {Base}_{D}$
49	48	elfvexd	$⊢ (φ \land P \in Inv (C)) \to D \in V$
50	16 17 8 49	catpropd	$⊢ (φ \land P \in Inv (C)) \to (C \in Cat \leftrightarrow D \in Cat)$
51	8 50	mpbid	$⊢ (φ \land P \in Inv (C)) \to D \in Cat$
52	42	simplrd	$⊢ (φ \land P \in Inv (C)) \to 2^{nd} (1^{st} (P)) \in {Base}_{C}$
53	52 47	eleqtrd	$⊢ (φ \land P \in Inv (C)) \to 2^{nd} (1^{st} (P)) \in {Base}_{D}$
54		eqid	$⊢ Sect (D) = Sect (D)$
55	44 45 51 48 53 54	invfval	$⊢ (φ \land P \in Inv (C)) \to 1^{st} (1^{st} (P)) Inv (D) 2^{nd} (1^{st} (P)) = (1^{st} (1^{st} (P)) Sect (D) 2^{nd} (1^{st} (P))) \cap {(2^{nd} (1^{st} (P)) Sect (D) 1^{st} (1^{st} (P)))}^{-1}$
56	22 43 55	3eqtr4rd	$⊢ (φ \land P \in Inv (C)) \to 1^{st} (1^{st} (P)) Inv (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P)$
57		invfn	$⊢ D \in Cat \to Inv (D) Fn ({Base}_{D} \times {Base}_{D})$
58	51 57	syl	$⊢ (φ \land P \in Inv (C)) \to Inv (D) Fn ({Base}_{D} \times {Base}_{D})$
59		fnbrovb	$⊢ (Inv (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)) Inv (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P) \leftrightarrow ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Inv (D) 2^{nd} (P))$
60	58 48 53 59	syl12anc	$⊢ (φ \land P \in Inv (C)) \to (1^{st} (1^{st} (P)) Inv (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P) \leftrightarrow ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Inv (D) 2^{nd} (P))$
61	56 60	mpbid	$⊢ (φ \land P \in Inv (C)) \to ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Inv (D) 2^{nd} (P)$
62		df-br	$⊢ ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Inv (D) 2^{nd} (P) \leftrightarrow ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩ \in Inv (D)$
63	61 62	sylib	$⊢ (φ \land P \in Inv (C)) \to ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩ \in Inv (D)$
64	15 63	eqeltrd	$⊢ (φ \land P \in Inv (C)) \to P \in Inv (D)$

Metamath Proof Explorer

Theorem invpropdlem

Proof