isoval

Description: The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof shortened by AV, 21-May-2020)

	Ref	Expression
Hypotheses	invfval.b	$⊢ B = {Base}_{C}$
	invfval.n	$⊢ N = Inv (C)$
	invfval.c	$⊢ φ \to C \in Cat$
	invss.x	$⊢ φ \to X \in B$
	invss.y	$⊢ φ \to Y \in B$
	isoval.n	$⊢ I = Iso (C)$
Assertion	isoval	$⊢ φ \to X I Y = dom (X N Y)$

Proof

Step	Hyp	Ref	Expression
1		invfval.b	$⊢ B = {Base}_{C}$
2		invfval.n	$⊢ N = Inv (C)$
3		invfval.c	$⊢ φ \to C \in Cat$
4		invss.x	$⊢ φ \to X \in B$
5		invss.y	$⊢ φ \to Y \in B$
6		isoval.n	$⊢ I = Iso (C)$
7		isofval	$⊢ C \in Cat \to Iso (C) = (z \in V ⟼ dom z) \circ Inv (C)$
8	3 7	syl	$⊢ φ \to Iso (C) = (z \in V ⟼ dom z) \circ Inv (C)$
9	2	coeq2i	$⊢ (z \in V ⟼ dom z) \circ N = (z \in V ⟼ dom z) \circ Inv (C)$
10	8 6 9	3eqtr4g	$⊢ φ \to I = (z \in V ⟼ dom z) \circ N$
11	10	oveqd	$⊢ φ \to X I Y = X ((z \in V ⟼ dom z) \circ N) Y$
12		eqid	$⊢ (x \in B, y \in B ⟼ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1}) = (x \in B, y \in B ⟼ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})$
13		ovex	$⊢ x Sect (C) y \in V$
14	13	inex1	$⊢ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1} \in V$
15	12 14	fnmpoi	$⊢ (x \in B, y \in B ⟼ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1}) Fn (B \times B)$
16		eqid	$⊢ Sect (C) = Sect (C)$
17	1 2 3 16	invffval	$⊢ φ \to N = (x \in B, y \in B ⟼ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1})$
18	17	fneq1d	$⊢ φ \to (N Fn (B \times B) \leftrightarrow (x \in B, y \in B ⟼ (x Sect (C) y) \cap {(y Sect (C) x)}^{-1}) Fn (B \times B))$
19	15 18	mpbiri	$⊢ φ \to N Fn (B \times B)$
20	4 5	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
21		fvco2	$⊢ (N Fn (B \times B) \land ⟨X, Y⟩ \in (B \times B)) \to ((z \in V ⟼ dom z) \circ N) (⟨X, Y⟩) = (z \in V ⟼ dom z) (N (⟨X, Y⟩))$
22	19 20 21	syl2anc	$⊢ φ \to ((z \in V ⟼ dom z) \circ N) (⟨X, Y⟩) = (z \in V ⟼ dom z) (N (⟨X, Y⟩))$
23		df-ov	$⊢ X ((z \in V ⟼ dom z) \circ N) Y = ((z \in V ⟼ dom z) \circ N) (⟨X, Y⟩)$
24		ovex	$⊢ X N Y \in V$
25		dmeq	$⊢ z = X N Y \to dom z = dom (X N Y)$
26		eqid	$⊢ (z \in V ⟼ dom z) = (z \in V ⟼ dom z)$
27	24	dmex	$⊢ dom (X N Y) \in V$
28	25 26 27	fvmpt	$⊢ X N Y \in V \to (z \in V ⟼ dom z) (X N Y) = dom (X N Y)$
29	24 28	ax-mp	$⊢ (z \in V ⟼ dom z) (X N Y) = dom (X N Y)$
30		df-ov	$⊢ X N Y = N (⟨X, Y⟩)$
31	30	fveq2i	$⊢ (z \in V ⟼ dom z) (X N Y) = (z \in V ⟼ dom z) (N (⟨X, Y⟩))$
32	29 31	eqtr3i	$⊢ dom (X N Y) = (z \in V ⟼ dom z) (N (⟨X, Y⟩))$
33	22 23 32	3eqtr4g	$⊢ φ \to X ((z \in V ⟼ dom z) \circ N) Y = dom (X N Y)$
34	11 33	eqtrd	$⊢ φ \to X I Y = dom (X N Y)$

Metamath Proof Explorer

Theorem isoval

Proof