xpcomco

Description: Composition with the bijection of xpcomf1o swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Hypotheses	xpcomf1o.1	$⊢ F = (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1})$
	xpcomco.1	$⊢ G = (y \in B, z \in A ⟼ C)$
Assertion	xpcomco	$⊢ G \circ F = (z \in A, y \in B ⟼ C)$

Proof

Step	Hyp	Ref	Expression
1		xpcomf1o.1	$⊢ F = (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1})$
2		xpcomco.1	$⊢ G = (y \in B, z \in A ⟼ C)$
3	1	xpcomf1o	$⊢ F : A \times B \underset{1-1 onto}{⟶} B \times A$
4		f1ofun	$⊢ F : A \times B \underset{1-1 onto}{⟶} B \times A \to Fun F$
5		funbrfv2b	$⊢ Fun F \to (u F w \leftrightarrow (u \in dom F \land F (u) = w))$
6	3 4 5	mp2b	$⊢ u F w \leftrightarrow (u \in dom F \land F (u) = w)$
7		ancom	$⊢ (u \in dom F \land F (u) = w) \leftrightarrow (F (u) = w \land u \in dom F)$
8		eqcom	$⊢ F (u) = w \leftrightarrow w = F (u)$
9		f1odm	$⊢ F : A \times B \underset{1-1 onto}{⟶} B \times A \to dom F = A \times B$
10	3 9	ax-mp	$⊢ dom F = A \times B$
11	10	eleq2i	$⊢ u \in dom F \leftrightarrow u \in (A \times B)$
12	8 11	anbi12i	$⊢ (F (u) = w \land u \in dom F) \leftrightarrow (w = F (u) \land u \in (A \times B))$
13	6 7 12	3bitri	$⊢ u F w \leftrightarrow (w = F (u) \land u \in (A \times B))$
14	13	anbi1i	$⊢ (u F w \land w G v) \leftrightarrow ((w = F (u) \land u \in (A \times B)) \land w G v)$
15		anass	$⊢ ((w = F (u) \land u \in (A \times B)) \land w G v) \leftrightarrow (w = F (u) \land (u \in (A \times B) \land w G v))$
16	14 15	bitri	$⊢ (u F w \land w G v) \leftrightarrow (w = F (u) \land (u \in (A \times B) \land w G v))$
17	16	exbii	$⊢ \exists w (u F w \land w G v) \leftrightarrow \exists w (w = F (u) \land (u \in (A \times B) \land w G v))$
18		fvex	$⊢ F (u) \in V$
19		breq1	$⊢ w = F (u) \to (w G v \leftrightarrow F (u) G v)$
20	19	anbi2d	$⊢ w = F (u) \to ((u \in (A \times B) \land w G v) \leftrightarrow (u \in (A \times B) \land F (u) G v))$
21	18 20	ceqsexv	$⊢ \exists w (w = F (u) \land (u \in (A \times B) \land w G v)) \leftrightarrow (u \in (A \times B) \land F (u) G v)$
22		elxp	$⊢ u \in (A \times B) \leftrightarrow \exists z \exists y (u = ⟨z, y⟩ \land (z \in A \land y \in B))$
23	22	anbi1i	$⊢ (u \in (A \times B) \land F (u) G v) \leftrightarrow (\exists z \exists y (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v)$
24		nfcv	$⊢ \underline{Ⅎ} z F (u)$
25		nfmpo2	$⊢ \underline{Ⅎ} z (y \in B, z \in A ⟼ C)$
26	2 25	nfcxfr	$⊢ \underline{Ⅎ} z G$
27		nfcv	$⊢ \underline{Ⅎ} z v$
28	24 26 27	nfbr	$⊢ Ⅎ z F (u) G v$
29	28	19.41	$⊢ \exists z (\exists y (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v) \leftrightarrow (\exists z \exists y (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v)$
30		nfcv	$⊢ \underline{Ⅎ} y F (u)$
31		nfmpo1	$⊢ \underline{Ⅎ} y (y \in B, z \in A ⟼ C)$
32	2 31	nfcxfr	$⊢ \underline{Ⅎ} y G$
33		nfcv	$⊢ \underline{Ⅎ} y v$
34	30 32 33	nfbr	$⊢ Ⅎ y F (u) G v$
35	34	19.41	$⊢ \exists y ((u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v) \leftrightarrow (\exists y (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v)$
36		anass	$⊢ ((u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v) \leftrightarrow (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land F (u) G v))$
37		fveq2	$⊢ u = ⟨z, y⟩ \to F (u) = F (⟨z, y⟩)$
38		opelxpi	$⊢ (z \in A \land y \in B) \to ⟨z, y⟩ \in (A \times B)$
39		sneq	$⊢ x = ⟨z, y⟩ \to \{x\} = \{⟨z, y⟩\}$
40	39	cnveqd	$⊢ x = ⟨z, y⟩ \to {\{x\}}^{-1} = {\{⟨z, y⟩\}}^{-1}$
41	40	unieqd	$⊢ x = ⟨z, y⟩ \to ⋃ {\{x\}}^{-1} = ⋃ {\{⟨z, y⟩\}}^{-1}$
42		opswap	$⊢ ⋃ {\{⟨z, y⟩\}}^{-1} = ⟨y, z⟩$
43	41 42	syl6eq	$⊢ x = ⟨z, y⟩ \to ⋃ {\{x\}}^{-1} = ⟨y, z⟩$
44		opex	$⊢ ⟨y, z⟩ \in V$
45	43 1 44	fvmpt	$⊢ ⟨z, y⟩ \in (A \times B) \to F (⟨z, y⟩) = ⟨y, z⟩$
46	38 45	syl	$⊢ (z \in A \land y \in B) \to F (⟨z, y⟩) = ⟨y, z⟩$
47	37 46	sylan9eq	$⊢ (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \to F (u) = ⟨y, z⟩$
48	47	breq1d	$⊢ (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \to (F (u) G v \leftrightarrow ⟨y, z⟩ G v)$
49		df-br	$⊢ ⟨y, z⟩ G v \leftrightarrow ⟨⟨y, z⟩, v⟩ \in G$
50		df-mpo	$⊢ (y \in B, z \in A ⟼ C) = \{⟨⟨y, z⟩, v⟩ \| ((y \in B \land z \in A) \land v = C)\}$
51	2 50	eqtri	$⊢ G = \{⟨⟨y, z⟩, v⟩ \| ((y \in B \land z \in A) \land v = C)\}$
52	51	eleq2i	$⊢ ⟨⟨y, z⟩, v⟩ \in G \leftrightarrow ⟨⟨y, z⟩, v⟩ \in \{⟨⟨y, z⟩, v⟩ \| ((y \in B \land z \in A) \land v = C)\}$
53		oprabidw	$⊢ ⟨⟨y, z⟩, v⟩ \in \{⟨⟨y, z⟩, v⟩ \| ((y \in B \land z \in A) \land v = C)\} \leftrightarrow ((y \in B \land z \in A) \land v = C)$
54	49 52 53	3bitri	$⊢ ⟨y, z⟩ G v \leftrightarrow ((y \in B \land z \in A) \land v = C)$
55	54	baib	$⊢ (y \in B \land z \in A) \to (⟨y, z⟩ G v \leftrightarrow v = C)$
56	55	ancoms	$⊢ (z \in A \land y \in B) \to (⟨y, z⟩ G v \leftrightarrow v = C)$
57	56	adantl	$⊢ (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \to (⟨y, z⟩ G v \leftrightarrow v = C)$
58	48 57	bitrd	$⊢ (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \to (F (u) G v \leftrightarrow v = C)$
59	58	pm5.32da	$⊢ u = ⟨z, y⟩ \to (((z \in A \land y \in B) \land F (u) G v) \leftrightarrow ((z \in A \land y \in B) \land v = C))$
60	59	pm5.32i	$⊢ (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land F (u) G v)) \leftrightarrow (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))$
61	36 60	bitri	$⊢ ((u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v) \leftrightarrow (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))$
62	61	exbii	$⊢ \exists y ((u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v) \leftrightarrow \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))$
63	35 62	bitr3i	$⊢ (\exists y (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v) \leftrightarrow \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))$
64	63	exbii	$⊢ \exists z (\exists y (u = ⟨z, y⟩ \land (z \in A \land y \in B)) \land F (u) G v) \leftrightarrow \exists z \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))$
65	23 29 64	3bitr2i	$⊢ (u \in (A \times B) \land F (u) G v) \leftrightarrow \exists z \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))$
66	17 21 65	3bitri	$⊢ \exists w (u F w \land w G v) \leftrightarrow \exists z \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))$
67	66	opabbii	$⊢ \{⟨u, v⟩ \| \exists w (u F w \land w G v)\} = \{⟨u, v⟩ \| \exists z \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))\}$
68		df-co	$⊢ G \circ F = \{⟨u, v⟩ \| \exists w (u F w \land w G v)\}$
69		df-mpo	$⊢ (z \in A, y \in B ⟼ C) = \{⟨⟨z, y⟩, v⟩ \| ((z \in A \land y \in B) \land v = C)\}$
70		dfoprab2	$⊢ \{⟨⟨z, y⟩, v⟩ \| ((z \in A \land y \in B) \land v = C)\} = \{⟨u, v⟩ \| \exists z \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))\}$
71	69 70	eqtri	$⊢ (z \in A, y \in B ⟼ C) = \{⟨u, v⟩ \| \exists z \exists y (u = ⟨z, y⟩ \land ((z \in A \land y \in B) \land v = C))\}$
72	67 68 71	3eqtr4i	$⊢ G \circ F = (z \in A, y \in B ⟼ C)$

Metamath Proof Explorer

Theorem xpcomco

Proof