pmtrmvd

Description: A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015)

		Ref	Expression
	Hypothesis	pmtrfval.t	$⊢ T = pmTrsp (D)$
	Assertion	pmtrmvd	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to dom (T (P) ∖ I) = P$

Proof

Step	Hyp	Ref	Expression
1		pmtrfval.t	$⊢ T = pmTrsp (D)$
2	1	pmtrf	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to T (P) : D ⟶ D$
3		ffn	$⊢ T (P) : D ⟶ D \to T (P) Fn D$
4		fndifnfp	$⊢ T (P) Fn D \to dom (T (P) ∖ I) = \{z \in D \| T (P) (z) \neq z\}$
5	2 3 4	3syl	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to dom (T (P) ∖ I) = \{z \in D \| T (P) (z) \neq z\}$
6	1	pmtrfv	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \to T (P) (z) = if (z \in P, ⋃ (P ∖ \{z\}), z)$
7	6	neeq1d	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \to (T (P) (z) \neq z \leftrightarrow if (z \in P, ⋃ (P ∖ \{z\}), z) \neq z)$
8		iffalse	$⊢ \neg z \in P \to if (z \in P, ⋃ (P ∖ \{z\}), z) = z$
9	8	necon1ai	$⊢ if (z \in P, ⋃ (P ∖ \{z\}), z) \neq z \to z \in P$
10		iftrue	$⊢ z \in P \to if (z \in P, ⋃ (P ∖ \{z\}), z) = ⋃ (P ∖ \{z\})$
11	10	adantl	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in P) \to if (z \in P, ⋃ (P ∖ \{z\}), z) = ⋃ (P ∖ \{z\})$
12		1onn	$⊢ 1_{𝑜} \in ω$
13		simpl3	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in P) \to P \approx 2_{𝑜}$
14		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
15	13 14	breqtrdi	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in P) \to P \approx suc 1_{𝑜}$
16		simpr	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in P) \to z \in P$
17		dif1ennn	$⊢ (1_{𝑜} \in ω \land P \approx suc 1_{𝑜} \land z \in P) \to (P ∖ \{z\}) \approx 1_{𝑜}$
18	12 15 16 17	mp3an2i	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in P) \to (P ∖ \{z\}) \approx 1_{𝑜}$
19		en1uniel	$⊢ (P ∖ \{z\}) \approx 1_{𝑜} \to ⋃ (P ∖ \{z\}) \in (P ∖ \{z\})$
20		eldifsni	$⊢ ⋃ (P ∖ \{z\}) \in (P ∖ \{z\}) \to ⋃ (P ∖ \{z\}) \neq z$
21	18 19 20	3syl	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in P) \to ⋃ (P ∖ \{z\}) \neq z$
22	11 21	eqnetrd	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in P) \to if (z \in P, ⋃ (P ∖ \{z\}), z) \neq z$
23	22	ex	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to (z \in P \to if (z \in P, ⋃ (P ∖ \{z\}), z) \neq z)$
24	9 23	impbid2	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to (if (z \in P, ⋃ (P ∖ \{z\}), z) \neq z \leftrightarrow z \in P)$
25	24	adantr	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \to (if (z \in P, ⋃ (P ∖ \{z\}), z) \neq z \leftrightarrow z \in P)$
26	7 25	bitrd	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \to (T (P) (z) \neq z \leftrightarrow z \in P)$
27	26	rabbidva	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to \{z \in D \| T (P) (z) \neq z\} = \{z \in D \| z \in P\}$
28		incom	$⊢ P \cap D = D \cap P$
29		dfin5	$⊢ D \cap P = \{z \in D \| z \in P\}$
30	28 29	eqtri	$⊢ P \cap D = \{z \in D \| z \in P\}$
31	27 30	eqtr4di	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to \{z \in D \| T (P) (z) \neq z\} = P \cap D$
32		simp2	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to P \subseteq D$
33		dfss2	$⊢ P \subseteq D \leftrightarrow P \cap D = P$
34	32 33	sylib	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to P \cap D = P$
35	5 31 34	3eqtrd	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to dom (T (P) ∖ I) = P$

Metamath Proof Explorer

Theorem pmtrmvd

Proof