f1otrspeq

Description: A transposition is characterized by the points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015)

		Ref	Expression
	Assertion	f1otrspeq	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to F = G$

Proof

Step	Hyp	Ref	Expression
1		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} A \to F Fn A$
2	1	ad2antrr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to F Fn A$
3		f1ofn	$⊢ G : A \underset{1-1 onto}{⟶} A \to G Fn A$
4	3	ad2antlr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to G Fn A$
5		1onn	$⊢ 1_{𝑜} \in ω$
6		simplrr	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to dom (G ∖ I) = dom (F ∖ I)$
7		simplrl	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to dom (F ∖ I) \approx 2_{𝑜}$
8		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
9	7 8	breqtrdi	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to dom (F ∖ I) \approx suc 1_{𝑜}$
10	6 9	eqbrtrd	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to dom (G ∖ I) \approx suc 1_{𝑜}$
11		simpr	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to x \in dom (G ∖ I)$
12		dif1ennn	$⊢ (1_{𝑜} \in ω \land dom (G ∖ I) \approx suc 1_{𝑜} \land x \in dom (G ∖ I)) \to (dom (G ∖ I) ∖ \{x\}) \approx 1_{𝑜}$
13	5 10 11 12	mp3an2i	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to (dom (G ∖ I) ∖ \{x\}) \approx 1_{𝑜}$
14		euen1b	$⊢ (dom (G ∖ I) ∖ \{x\}) \approx 1_{𝑜} \leftrightarrow \exists! y y \in (dom (G ∖ I) ∖ \{x\})$
15		eumo	$⊢ \exists! y y \in (dom (G ∖ I) ∖ \{x\}) \to \exists^{*} y y \in (dom (G ∖ I) ∖ \{x\})$
16	14 15	sylbi	$⊢ (dom (G ∖ I) ∖ \{x\}) \approx 1_{𝑜} \to \exists^{*} y y \in (dom (G ∖ I) ∖ \{x\})$
17	13 16	syl	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to \exists^{*} y y \in (dom (G ∖ I) ∖ \{x\})$
18		f1omvdmvd	$⊢ (F : A \underset{1-1 onto}{⟶} A \land x \in dom (F ∖ I)) \to F (x) \in (dom (F ∖ I) ∖ \{x\})$
19	18	ex	$⊢ F : A \underset{1-1 onto}{⟶} A \to (x \in dom (F ∖ I) \to F (x) \in (dom (F ∖ I) ∖ \{x\}))$
20	19	ad2antrr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to (x \in dom (F ∖ I) \to F (x) \in (dom (F ∖ I) ∖ \{x\}))$
21		eleq2	$⊢ dom (G ∖ I) = dom (F ∖ I) \to (x \in dom (G ∖ I) \leftrightarrow x \in dom (F ∖ I))$
22	21	ad2antll	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to (x \in dom (G ∖ I) \leftrightarrow x \in dom (F ∖ I))$
23		difeq1	$⊢ dom (G ∖ I) = dom (F ∖ I) \to dom (G ∖ I) ∖ \{x\} = dom (F ∖ I) ∖ \{x\}$
24	23	eleq2d	$⊢ dom (G ∖ I) = dom (F ∖ I) \to (F (x) \in (dom (G ∖ I) ∖ \{x\}) \leftrightarrow F (x) \in (dom (F ∖ I) ∖ \{x\}))$
25	24	ad2antll	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to (F (x) \in (dom (G ∖ I) ∖ \{x\}) \leftrightarrow F (x) \in (dom (F ∖ I) ∖ \{x\}))$
26	20 22 25	3imtr4d	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to (x \in dom (G ∖ I) \to F (x) \in (dom (G ∖ I) ∖ \{x\}))$
27	26	imp	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to F (x) \in (dom (G ∖ I) ∖ \{x\})$
28		f1omvdmvd	$⊢ (G : A \underset{1-1 onto}{⟶} A \land x \in dom (G ∖ I)) \to G (x) \in (dom (G ∖ I) ∖ \{x\})$
29	28	ad4ant24	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to G (x) \in (dom (G ∖ I) ∖ \{x\})$
30		fvex	$⊢ F (x) \in V$
31		fvex	$⊢ G (x) \in V$
32	30 31	pm3.2i	$⊢ (F (x) \in V \land G (x) \in V)$
33		eleq1	$⊢ y = F (x) \to (y \in (dom (G ∖ I) ∖ \{x\}) \leftrightarrow F (x) \in (dom (G ∖ I) ∖ \{x\}))$
34		eleq1	$⊢ y = G (x) \to (y \in (dom (G ∖ I) ∖ \{x\}) \leftrightarrow G (x) \in (dom (G ∖ I) ∖ \{x\}))$
35	33 34	moi	$⊢ ((F (x) \in V \land G (x) \in V) \land \exists^{*} y y \in (dom (G ∖ I) ∖ \{x\}) \land (F (x) \in (dom (G ∖ I) ∖ \{x\}) \land G (x) \in (dom (G ∖ I) ∖ \{x\}))) \to F (x) = G (x)$
36	32 35	mp3an1	$⊢ (\exists^{*} y y \in (dom (G ∖ I) ∖ \{x\}) \land (F (x) \in (dom (G ∖ I) ∖ \{x\}) \land G (x) \in (dom (G ∖ I) ∖ \{x\}))) \to F (x) = G (x)$
37	17 27 29 36	syl12anc	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in dom (G ∖ I)) \to F (x) = G (x)$
38	37	adantlr	$⊢ ((((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \land x \in dom (G ∖ I)) \to F (x) = G (x)$
39		simplrr	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to dom (G ∖ I) = dom (F ∖ I)$
40	39	eleq2d	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to (x \in dom (G ∖ I) \leftrightarrow x \in dom (F ∖ I))$
41		fnelnfp	$⊢ (F Fn A \land x \in A) \to (x \in dom (F ∖ I) \leftrightarrow F (x) \neq x)$
42	2 41	sylan	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to (x \in dom (F ∖ I) \leftrightarrow F (x) \neq x)$
43	40 42	bitrd	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to (x \in dom (G ∖ I) \leftrightarrow F (x) \neq x)$
44	43	necon2bbid	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to (F (x) = x \leftrightarrow \neg x \in dom (G ∖ I))$
45	44	biimpar	$⊢ ((((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \land \neg x \in dom (G ∖ I)) \to F (x) = x$
46		fnelnfp	$⊢ (G Fn A \land x \in A) \to (x \in dom (G ∖ I) \leftrightarrow G (x) \neq x)$
47	4 46	sylan	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to (x \in dom (G ∖ I) \leftrightarrow G (x) \neq x)$
48	47	necon2bbid	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to (G (x) = x \leftrightarrow \neg x \in dom (G ∖ I))$
49	48	biimpar	$⊢ ((((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \land \neg x \in dom (G ∖ I)) \to G (x) = x$
50	45 49	eqtr4d	$⊢ ((((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \land \neg x \in dom (G ∖ I)) \to F (x) = G (x)$
51	38 50	pm2.61dan	$⊢ (((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \land x \in A) \to F (x) = G (x)$
52	2 4 51	eqfnfvd	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (G ∖ I) = dom (F ∖ I))) \to F = G$

Metamath Proof Explorer

Theorem f1otrspeq

Proof