trsp2cyc

Description: Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023)

	Ref	Expression
Hypotheses	trsp2cyc.t	$⊢ T = ran pmTrsp (D)$
	trsp2cyc.c	$⊢ C = toCyc (D)$
Assertion	trsp2cyc	$⊢ (D \in V \land P \in T) \to \exists i \in D \exists j \in D (i \neq j \land P = C (⟨“ i j ”⟩))$

Proof

Step	Hyp	Ref	Expression
1		trsp2cyc.t	$⊢ T = ran pmTrsp (D)$
2		trsp2cyc.c	$⊢ C = toCyc (D)$
3		simplr	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}$
4		breq1	$⊢ y = p \to (y \approx 2_{𝑜} \leftrightarrow p \approx 2_{𝑜})$
5	4	elrab	$⊢ p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} \leftrightarrow (p \in 𝒫 D \land p \approx 2_{𝑜})$
6	3 5	sylib	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to (p \in 𝒫 D \land p \approx 2_{𝑜})$
7	6	simprd	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to p \approx 2_{𝑜}$
8		en2	$⊢ p \approx 2_{𝑜} \to \exists i \exists j p = \{i, j\}$
9	7 8	syl	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to \exists i \exists j p = \{i, j\}$
10	6	simpld	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to p \in 𝒫 D$
11	10	elpwid	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to p \subseteq D$
12	11	adantr	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to p \subseteq D$
13		vex	$⊢ i \in V$
14	13	prid1	$⊢ i \in \{i, j\}$
15		simpr	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to p = \{i, j\}$
16	14 15	eleqtrrid	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to i \in p$
17	12 16	sseldd	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to i \in D$
18		vex	$⊢ j \in V$
19	18	prid2	$⊢ j \in \{i, j\}$
20	19 15	eleqtrrid	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to j \in p$
21	12 20	sseldd	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to j \in D$
22	7	adantr	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to p \approx 2_{𝑜}$
23	15 22	eqbrtrrd	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to \{i, j\} \approx 2_{𝑜}$
24		pr2ne	$⊢ (i \in D \land j \in D) \to (\{i, j\} \approx 2_{𝑜} \leftrightarrow i \neq j)$
25	24	biimpa	$⊢ ((i \in D \land j \in D) \land \{i, j\} \approx 2_{𝑜}) \to i \neq j$
26	17 21 23 25	syl21anc	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to i \neq j$
27		simplr	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))$
28		simp-4l	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to D \in V$
29		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
30	29	pmtrval	$⊢ (D \in V \land p \subseteq D \land p \approx 2_{𝑜}) \to pmTrsp (D) (p) = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))$
31	28 12 22 30	syl3anc	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to pmTrsp (D) (p) = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))$
32	15	fveq2d	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to pmTrsp (D) (p) = pmTrsp (D) (\{i, j\})$
33	27 31 32	3eqtr2d	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to P = pmTrsp (D) (\{i, j\})$
34	2 28 17 21 26 29	cycpm2tr	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to C (⟨“ i j ”⟩) = pmTrsp (D) (\{i, j\})$
35	33 34	eqtr4d	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to P = C (⟨“ i j ”⟩)$
36	26 35	jca	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to (i \neq j \land P = C (⟨“ i j ”⟩))$
37	17 21 36	jca31	$⊢ ((((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \land p = \{i, j\}) \to ((i \in D \land j \in D) \land (i \neq j \land P = C (⟨“ i j ”⟩)))$
38	37	ex	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to (p = \{i, j\} \to ((i \in D \land j \in D) \land (i \neq j \land P = C (⟨“ i j ”⟩))))$
39	38	2eximdv	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to (\exists i \exists j p = \{i, j\} \to \exists i \exists j ((i \in D \land j \in D) \land (i \neq j \land P = C (⟨“ i j ”⟩))))$
40	9 39	mpd	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to \exists i \exists j ((i \in D \land j \in D) \land (i \neq j \land P = C (⟨“ i j ”⟩)))$
41		r2ex	$⊢ \exists i \in D \exists j \in D (i \neq j \land P = C (⟨“ i j ”⟩)) \leftrightarrow \exists i \exists j ((i \in D \land j \in D) \land (i \neq j \land P = C (⟨“ i j ”⟩)))$
42	40 41	sylibr	$⊢ (((D \in V \land P \in T) \land p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\}) \land P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \to \exists i \in D \exists j \in D (i \neq j \land P = C (⟨“ i j ”⟩))$
43		simpr	$⊢ (D \in V \land P \in T) \to P \in T$
44	29	pmtrfval	$⊢ D \in V \to pmTrsp (D) = (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
45	44	adantr	$⊢ (D \in V \land P \in T) \to pmTrsp (D) = (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
46	45	rneqd	$⊢ (D \in V \land P \in T) \to ran pmTrsp (D) = ran (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
47	1 46	syl5eq	$⊢ (D \in V \land P \in T) \to T = ran (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
48	43 47	eleqtrd	$⊢ (D \in V \land P \in T) \to P \in ran (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
49		eqid	$⊢ (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) = (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
50	49	elrnmpt	$⊢ P \in T \to (P \in ran (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \leftrightarrow \exists p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
51	50	adantl	$⊢ (D \in V \land P \in T) \to (P \in ran (p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} ⟼ (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))) \leftrightarrow \exists p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z)))$
52	48 51	mpbid	$⊢ (D \in V \land P \in T) \to \exists p \in \{y \in 𝒫 D \| y \approx 2_{𝑜}\} P = (z \in D ⟼ if (z \in p, ⋃ (p ∖ \{z\}), z))$
53	42 52	r19.29a	$⊢ (D \in V \land P \in T) \to \exists i \in D \exists j \in D (i \neq j \land P = C (⟨“ i j ”⟩))$

Metamath Proof Explorer

Theorem trsp2cyc

Proof