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 ) )