Metamath Proof Explorer

Theorem pmtrfinv

Description: A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrrn.r ⊢ 𝑅 = ran 𝑇
Assertion pmtrfinv ( 𝐹 ∈ 𝑅 → ( 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐷 ) )

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 4 simpld ⊢ ( 𝐹 ∈ 𝑅 → ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )
6 1 pmtrf ⊢ ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 )
7 5 6 syl ⊢ ( 𝐹 ∈ 𝑅 → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 )
8 4 simprd ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) )
9 8 feq1d ⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 : 𝐷 ⟶ 𝐷 ↔ ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 ) )
10 7 9 mpbird ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 : 𝐷 ⟶ 𝐷 )
11 fco ⊢ ( ( 𝐹 : 𝐷 ⟶ 𝐷 ∧ 𝐹 : 𝐷 ⟶ 𝐷 ) → ( 𝐹 ∘ 𝐹 ) : 𝐷 ⟶ 𝐷 )
12 11 anidms ⊢ ( 𝐹 : 𝐷 ⟶ 𝐷 → ( 𝐹 ∘ 𝐹 ) : 𝐷 ⟶ 𝐷 )
13 ffn ⊢ ( ( 𝐹 ∘ 𝐹 ) : 𝐷 ⟶ 𝐷 → ( 𝐹 ∘ 𝐹 ) Fn 𝐷 )
14 10 12 13 3syl ⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 ∘ 𝐹 ) Fn 𝐷 )
15 fnresi ⊢ ( I ↾ 𝐷 ) Fn 𝐷
16 15 a1i ⊢ ( 𝐹 ∈ 𝑅 → ( I ↾ 𝐷 ) Fn 𝐷 )
17 1 2 3 pmtrffv ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ dom ( 𝐹 ∖ I ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
18 iftrue ⊢ ( 𝑥 ∈ dom ( 𝐹 ∖ I ) → if ( 𝑥 ∈ dom ( 𝐹 ∖ I ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) = ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) )
19 17 18 sylan9eq ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) = ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) )
20 19 fveq2d ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) )
21 simpll ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → 𝐹 ∈ 𝑅 )
22 5 simp2d ⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ⊆ 𝐷 )
23 22 ad2antrr ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → dom ( 𝐹 ∖ I ) ⊆ 𝐷 )
24 1onn ⊢ 1o ∈ ω
25 5 simp3d ⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ≈ 2o )
26 df-2o ⊢ 2o = suc 1o
27 25 26 breqtrdi ⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ≈ suc 1o )
28 27 ad2antrr ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → dom ( 𝐹 ∖ I ) ≈ suc 1o )
29 simpr ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → 𝑥 ∈ dom ( 𝐹 ∖ I ) )
30 dif1ennn ⊢ ( ( 1o ∈ ω ∧ dom ( 𝐹 ∖ I ) ≈ suc 1o ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ≈ 1o )
31 24 28 29 30 mp3an2i ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ≈ 1o )
32 en1uniel ⊢ ( ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ≈ 1o → ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) )
33 31 32 syl ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) )
34 33 eldifad ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ dom ( 𝐹 ∖ I ) )
35 23 34 sseldd ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ 𝐷 )
36 1 2 3 pmtrffv ⊢ ( ( 𝐹 ∈ 𝑅 ∧ ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ 𝐷 ) → ( 𝐹 ‘ ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) = if ( ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ dom ( 𝐹 ∖ I ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) )
37 21 35 36 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) = if ( ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ dom ( 𝐹 ∖ I ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) )
38 iftrue ⊢ ( ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ dom ( 𝐹 ∖ I ) → if ( ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ dom ( 𝐹 ∖ I ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) = ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) )
39 34 38 syl ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → if ( ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ dom ( 𝐹 ∖ I ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) = ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) )
40 25 adantr ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → dom ( 𝐹 ∖ I ) ≈ 2o )
41 en2other2 ⊢ ( ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) = 𝑥 )
42 41 ancoms ⊢ ( ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) = 𝑥 )
43 40 42 sylan ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) = 𝑥 )
44 39 43 eqtrd ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → if ( ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ∈ dom ( 𝐹 ∖ I ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) } ) , ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) = 𝑥 )
45 37 44 eqtrd ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ ∪ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) = 𝑥 )
46 20 45 eqtrd ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
47 10 ffnd ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 Fn 𝐷 )
48 fnelnfp ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) )
49 47 48 sylan ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) )
50 49 necon2bbid ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) )
51 50 biimpar ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
52 fveq2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
53 id ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
54 52 53 eqtrd ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
55 51 54 syl ⊢ ( ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
56 46 55 pm2.61dan ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
57 fvco2 ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) )
58 47 57 sylan ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) )
59 fvresi ⊢ ( 𝑥 ∈ 𝐷 → ( ( I ↾ 𝐷 ) ‘ 𝑥 ) = 𝑥 )
60 59 adantl ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → ( ( I ↾ 𝐷 ) ‘ 𝑥 ) = 𝑥 )
61 56 58 60 3eqtr4d ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ∘ 𝐹 ) ‘ 𝑥 ) = ( ( I ↾ 𝐷 ) ‘ 𝑥 ) )
62 14 16 61 eqfnfvd ⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐷 ) )