pmtrfb

Description: An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Hypotheses	pmtrrn.t	$⊢ T = pmTrsp (D)$
	pmtrrn.r	$⊢ R = ran T$
Assertion	pmtrfb	$⊢ F \in R \leftrightarrow (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜})$

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		simpl1	$⊢ ((D \in V \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \approx 2_{𝑜}) \land F = T (dom (F ∖ I))) \to D \in V$
6	4 5	syl	$⊢ F \in R \to D \in V$
7	1 2	pmtrff1o	$⊢ F \in R \to F : D \underset{1-1 onto}{⟶} D$
8		simpl3	$⊢ ((D \in V \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \approx 2_{𝑜}) \land F = T (dom (F ∖ I))) \to dom (F ∖ I) \approx 2_{𝑜}$
9	4 8	syl	$⊢ F \in R \to dom (F ∖ I) \approx 2_{𝑜}$
10	6 7 9	3jca	$⊢ F \in R \to (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜})$
11		simp2	$⊢ (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜}) \to F : D \underset{1-1 onto}{⟶} D$
12		difss	$⊢ F ∖ I \subseteq F$
13		dmss	$⊢ F ∖ I \subseteq F \to dom (F ∖ I) \subseteq dom F$
14	12 13	ax-mp	$⊢ dom (F ∖ I) \subseteq dom F$
15		f1odm	$⊢ F : D \underset{1-1 onto}{⟶} D \to dom F = D$
16	14 15	sseqtrid	$⊢ F : D \underset{1-1 onto}{⟶} D \to dom (F ∖ I) \subseteq D$
17	1 2	pmtrrn	$⊢ (D \in V \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \approx 2_{𝑜}) \to T (dom (F ∖ I)) \in R$
18	16 17	syl3an2	$⊢ (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜}) \to T (dom (F ∖ I)) \in R$
19	1 2	pmtrff1o	$⊢ T (dom (F ∖ I)) \in R \to T (dom (F ∖ I)) : D \underset{1-1 onto}{⟶} D$
20	18 19	syl	$⊢ (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜}) \to T (dom (F ∖ I)) : D \underset{1-1 onto}{⟶} D$
21		simp3	$⊢ (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜}) \to dom (F ∖ I) \approx 2_{𝑜}$
22	1	pmtrmvd	$⊢ (D \in V \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \approx 2_{𝑜}) \to dom (T (dom (F ∖ I)) ∖ I) = dom (F ∖ I)$
23	16 22	syl3an2	$⊢ (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜}) \to dom (T (dom (F ∖ I)) ∖ I) = dom (F ∖ I)$
24		f1otrspeq	$⊢ ((F : D \underset{1-1 onto}{⟶} D \land T (dom (F ∖ I)) : D \underset{1-1 onto}{⟶} D) \land (dom (F ∖ I) \approx 2_{𝑜} \land dom (T (dom (F ∖ I)) ∖ I) = dom (F ∖ I))) \to F = T (dom (F ∖ I))$
25	11 20 21 23 24	syl22anc	$⊢ (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜}) \to F = T (dom (F ∖ I))$
26	25 18	eqeltrd	$⊢ (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜}) \to F \in R$
27	10 26	impbii	$⊢ F \in R \leftrightarrow (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜})$

Metamath Proof Explorer

Theorem pmtrfb

Proof