pmtrfinv

Description: A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Hypotheses	pmtrrn.t	$⊢ T = pmTrsp (D)$
	pmtrrn.r	$⊢ R = ran T$
Assertion	pmtrfinv	$⊢ F \in R \to F \circ F = {I ↾}_{D}$

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	$⊢ T = pmTrsp (D)$
2		pmtrrn.r	$⊢ R = ran T$
3		eqid	$⊢ dom (F ∖ I) = dom (F ∖ I)$
4	1 2 3	pmtrfrn	$⊢ F \in R \to ((D \in V \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \approx 2_{𝑜}) \land F = T (dom (F ∖ I)))$
5	4	simpld	$⊢ F \in R \to (D \in V \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \approx 2_{𝑜})$
6	1	pmtrf	$⊢ (D \in V \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \approx 2_{𝑜}) \to T (dom (F ∖ I)) : D ⟶ D$
7	5 6	syl	$⊢ F \in R \to T (dom (F ∖ I)) : D ⟶ D$
8	4	simprd	$⊢ F \in R \to F = T (dom (F ∖ I))$
9	8	feq1d	$⊢ F \in R \to (F : D ⟶ D \leftrightarrow T (dom (F ∖ I)) : D ⟶ D)$
10	7 9	mpbird	$⊢ F \in R \to F : D ⟶ D$
11		fco	$⊢ (F : D ⟶ D \land F : D ⟶ D) \to (F \circ F) : D ⟶ D$
12	11	anidms	$⊢ F : D ⟶ D \to (F \circ F) : D ⟶ D$
13		ffn	$⊢ (F \circ F) : D ⟶ D \to (F \circ F) Fn D$
14	10 12 13	3syl	$⊢ F \in R \to (F \circ F) Fn D$
15		fnresi	$⊢ ({I ↾}_{D}) Fn D$
16	15	a1i	$⊢ F \in R \to ({I ↾}_{D}) Fn D$
17	1 2 3	pmtrffv	$⊢ (F \in R \land x \in D) \to F (x) = if (x \in dom (F ∖ I), ⋃ (dom (F ∖ I) ∖ \{x\}), x)$
18		iftrue	$⊢ x \in dom (F ∖ I) \to if (x \in dom (F ∖ I), ⋃ (dom (F ∖ I) ∖ \{x\}), x) = ⋃ (dom (F ∖ I) ∖ \{x\})$
19	17 18	sylan9eq	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to F (x) = ⋃ (dom (F ∖ I) ∖ \{x\})$
20	19	fveq2d	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to F (F (x)) = F (⋃ (dom (F ∖ I) ∖ \{x\}))$
21		simpll	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to F \in R$
22	5	simp2d	$⊢ F \in R \to dom (F ∖ I) \subseteq D$
23	22	ad2antrr	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to dom (F ∖ I) \subseteq D$
24		1onn	$⊢ 1_{𝑜} \in ω$
25	5	simp3d	$⊢ F \in R \to dom (F ∖ I) \approx 2_{𝑜}$
26		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
27	25 26	breqtrdi	$⊢ F \in R \to dom (F ∖ I) \approx suc 1_{𝑜}$
28	27	ad2antrr	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to dom (F ∖ I) \approx suc 1_{𝑜}$
29		simpr	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to x \in dom (F ∖ I)$
30		dif1ennn	$⊢ (1_{𝑜} \in ω \land dom (F ∖ I) \approx suc 1_{𝑜} \land x \in dom (F ∖ I)) \to (dom (F ∖ I) ∖ \{x\}) \approx 1_{𝑜}$
31	24 28 29 30	mp3an2i	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to (dom (F ∖ I) ∖ \{x\}) \approx 1_{𝑜}$
32		en1uniel	$⊢ (dom (F ∖ I) ∖ \{x\}) \approx 1_{𝑜} \to ⋃ (dom (F ∖ I) ∖ \{x\}) \in (dom (F ∖ I) ∖ \{x\})$
33	31 32	syl	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to ⋃ (dom (F ∖ I) ∖ \{x\}) \in (dom (F ∖ I) ∖ \{x\})$
34	33	eldifad	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to ⋃ (dom (F ∖ I) ∖ \{x\}) \in dom (F ∖ I)$
35	23 34	sseldd	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to ⋃ (dom (F ∖ I) ∖ \{x\}) \in D$
36	1 2 3	pmtrffv	$⊢ (F \in R \land ⋃ (dom (F ∖ I) ∖ \{x\}) \in D) \to F (⋃ (dom (F ∖ I) ∖ \{x\})) = if (⋃ (dom (F ∖ I) ∖ \{x\}) \in dom (F ∖ I), ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}), ⋃ (dom (F ∖ I) ∖ \{x\}))$
37	21 35 36	syl2anc	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to F (⋃ (dom (F ∖ I) ∖ \{x\})) = if (⋃ (dom (F ∖ I) ∖ \{x\}) \in dom (F ∖ I), ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}), ⋃ (dom (F ∖ I) ∖ \{x\}))$
38		iftrue	$⊢ ⋃ (dom (F ∖ I) ∖ \{x\}) \in dom (F ∖ I) \to if (⋃ (dom (F ∖ I) ∖ \{x\}) \in dom (F ∖ I), ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}), ⋃ (dom (F ∖ I) ∖ \{x\})) = ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\})$
39	34 38	syl	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to if (⋃ (dom (F ∖ I) ∖ \{x\}) \in dom (F ∖ I), ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}), ⋃ (dom (F ∖ I) ∖ \{x\})) = ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\})$
40	25	adantr	$⊢ (F \in R \land x \in D) \to dom (F ∖ I) \approx 2_{𝑜}$
41		en2other2	$⊢ (x \in dom (F ∖ I) \land dom (F ∖ I) \approx 2_{𝑜}) \to ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}) = x$
42	41	ancoms	$⊢ (dom (F ∖ I) \approx 2_{𝑜} \land x \in dom (F ∖ I)) \to ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}) = x$
43	40 42	sylan	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}) = x$
44	39 43	eqtrd	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to if (⋃ (dom (F ∖ I) ∖ \{x\}) \in dom (F ∖ I), ⋃ (dom (F ∖ I) ∖ \{⋃ (dom (F ∖ I) ∖ \{x\})\}), ⋃ (dom (F ∖ I) ∖ \{x\})) = x$
45	37 44	eqtrd	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to F (⋃ (dom (F ∖ I) ∖ \{x\})) = x$
46	20 45	eqtrd	$⊢ ((F \in R \land x \in D) \land x \in dom (F ∖ I)) \to F (F (x)) = x$
47	10	ffnd	$⊢ F \in R \to F Fn D$
48		fnelnfp	$⊢ (F Fn D \land x \in D) \to (x \in dom (F ∖ I) \leftrightarrow F (x) \neq x)$
49	47 48	sylan	$⊢ (F \in R \land x \in D) \to (x \in dom (F ∖ I) \leftrightarrow F (x) \neq x)$
50	49	necon2bbid	$⊢ (F \in R \land x \in D) \to (F (x) = x \leftrightarrow \neg x \in dom (F ∖ I))$
51	50	biimpar	$⊢ ((F \in R \land x \in D) \land \neg x \in dom (F ∖ I)) \to F (x) = x$
52		fveq2	$⊢ F (x) = x \to F (F (x)) = F (x)$
53		id	$⊢ F (x) = x \to F (x) = x$
54	52 53	eqtrd	$⊢ F (x) = x \to F (F (x)) = x$
55	51 54	syl	$⊢ ((F \in R \land x \in D) \land \neg x \in dom (F ∖ I)) \to F (F (x)) = x$
56	46 55	pm2.61dan	$⊢ (F \in R \land x \in D) \to F (F (x)) = x$
57		fvco2	$⊢ (F Fn D \land x \in D) \to (F \circ F) (x) = F (F (x))$
58	47 57	sylan	$⊢ (F \in R \land x \in D) \to (F \circ F) (x) = F (F (x))$
59		fvresi	$⊢ x \in D \to ({I ↾}_{D}) (x) = x$
60	59	adantl	$⊢ (F \in R \land x \in D) \to ({I ↾}_{D}) (x) = x$
61	56 58 60	3eqtr4d	$⊢ (F \in R \land x \in D) \to (F \circ F) (x) = ({I ↾}_{D}) (x)$
62	14 16 61	eqfnfvd	$⊢ F \in R \to F \circ F = {I ↾}_{D}$

Metamath Proof Explorer

Theorem pmtrfinv

Proof