Metamath Proof Explorer


Theorem pmtrfb

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

Ref Expression
Hypotheses pmtrrn.t 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrrn.r 𝑅 = ran 𝑇
Assertion pmtrfb ( 𝐹𝑅 ↔ ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )

Proof

Step Hyp Ref Expression
1 pmtrrn.t 𝑇 = ( pmTrsp ‘ 𝐷 )
2 pmtrrn.r 𝑅 = ran 𝑇
3 eqid dom ( 𝐹 ∖ I ) = dom ( 𝐹 ∖ I )
4 1 2 3 pmtrfrn ( 𝐹𝑅 → ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) )
5 simpl1 ( ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) → 𝐷 ∈ V )
6 4 5 syl ( 𝐹𝑅𝐷 ∈ V )
7 1 2 pmtrff1o ( 𝐹𝑅𝐹 : 𝐷1-1-onto𝐷 )
8 simpl3 ( ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) → dom ( 𝐹 ∖ I ) ≈ 2o )
9 4 8 syl ( 𝐹𝑅 → dom ( 𝐹 ∖ I ) ≈ 2o )
10 6 7 9 3jca ( 𝐹𝑅 → ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )
11 simp2 ( ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → 𝐹 : 𝐷1-1-onto𝐷 )
12 difss ( 𝐹 ∖ I ) ⊆ 𝐹
13 dmss ( ( 𝐹 ∖ I ) ⊆ 𝐹 → dom ( 𝐹 ∖ I ) ⊆ dom 𝐹 )
14 12 13 ax-mp dom ( 𝐹 ∖ I ) ⊆ dom 𝐹
15 f1odm ( 𝐹 : 𝐷1-1-onto𝐷 → dom 𝐹 = 𝐷 )
16 14 15 sseqtrid ( 𝐹 : 𝐷1-1-onto𝐷 → dom ( 𝐹 ∖ I ) ⊆ 𝐷 )
17 1 2 pmtrrn ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ∈ 𝑅 )
18 16 17 syl3an2 ( ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ∈ 𝑅 )
19 1 2 pmtrff1o ( ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ∈ 𝑅 → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷1-1-onto𝐷 )
20 18 19 syl ( ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷1-1-onto𝐷 )
21 simp3 ( ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → dom ( 𝐹 ∖ I ) ≈ 2o )
22 1 pmtrmvd ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → dom ( ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ∖ I ) = dom ( 𝐹 ∖ I ) )
23 16 22 syl3an2 ( ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → dom ( ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ∖ I ) = dom ( 𝐹 ∖ I ) )
24 f1otrspeq ( ( ( 𝐹 : 𝐷1-1-onto𝐷 ∧ ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷1-1-onto𝐷 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) )
25 11 20 21 23 24 syl22anc ( ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) )
26 25 18 eqeltrd ( ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → 𝐹𝑅 )
27 10 26 impbii ( 𝐹𝑅 ↔ ( 𝐷 ∈ V ∧ 𝐹 : 𝐷1-1-onto𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )