Metamath Proof Explorer


Theorem pmtrfrn

Description: A transposition (as a kind of function) is the function transposing the two points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrrn.r 𝑅 = ran 𝑇
pmtrfrn.p 𝑃 = dom ( 𝐹 ∖ I )
Assertion pmtrfrn ( 𝐹𝑅 → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 pmtrrn.t 𝑇 = ( pmTrsp ‘ 𝐷 )
2 pmtrrn.r 𝑅 = ran 𝑇
3 pmtrfrn.p 𝑃 = dom ( 𝐹 ∖ I )
4 noel ¬ 𝐹 ∈ ∅
5 1 rnfvprc ( ¬ 𝐷 ∈ V → ran 𝑇 = ∅ )
6 2 5 eqtrid ( ¬ 𝐷 ∈ V → 𝑅 = ∅ )
7 6 eleq2d ( ¬ 𝐷 ∈ V → ( 𝐹𝑅𝐹 ∈ ∅ ) )
8 4 7 mtbiri ( ¬ 𝐷 ∈ V → ¬ 𝐹𝑅 )
9 8 con4i ( 𝐹𝑅𝐷 ∈ V )
10 mptexg ( 𝐷 ∈ V → ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V )
11 10 ralrimivw ( 𝐷 ∈ V → ∀ 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V )
12 eqid ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ↦ ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ↦ ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) )
13 12 fnmpt ( ∀ 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V → ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ↦ ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } )
14 11 13 syl ( 𝐷 ∈ V → ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ↦ ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } )
15 1 pmtrfval ( 𝐷 ∈ V → 𝑇 = ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ↦ ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
16 15 fneq1d ( 𝐷 ∈ V → ( 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ↔ ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ↦ ( 𝑧𝐷 ↦ if ( 𝑧𝑤 , ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ) )
17 14 16 mpbird ( 𝐷 ∈ V → 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } )
18 fvelrnb ( 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } → ( 𝐹 ∈ ran 𝑇 ↔ ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ( 𝑇𝑦 ) = 𝐹 ) )
19 17 18 syl ( 𝐷 ∈ V → ( 𝐹 ∈ ran 𝑇 ↔ ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ( 𝑇𝑦 ) = 𝐹 ) )
20 2 eleq2i ( 𝐹𝑅𝐹 ∈ ran 𝑇 )
21 breq1 ( 𝑥 = 𝑦 → ( 𝑥 ≈ 2o𝑦 ≈ 2o ) )
22 21 rexrab ( ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ( 𝑇𝑦 ) = 𝐹 ↔ ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇𝑦 ) = 𝐹 ) )
23 22 bicomi ( ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇𝑦 ) = 𝐹 ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷𝑥 ≈ 2o } ( 𝑇𝑦 ) = 𝐹 )
24 19 20 23 3bitr4g ( 𝐷 ∈ V → ( 𝐹𝑅 ↔ ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇𝑦 ) = 𝐹 ) ) )
25 elpwi ( 𝑦 ∈ 𝒫 𝐷𝑦𝐷 )
26 simp1 ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → 𝐷 ∈ V )
27 1 pmtrmvd ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑦 )
28 simp2 ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → 𝑦𝐷 )
29 27 28 eqsstrd ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷 )
30 simp3 ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → 𝑦 ≈ 2o )
31 27 30 eqbrtrd ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o )
32 26 29 31 3jca ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → ( 𝐷 ∈ V ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o ) )
33 27 eqcomd ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → 𝑦 = dom ( ( 𝑇𝑦 ) ∖ I ) )
34 33 fveq2d ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → ( 𝑇𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇𝑦 ) ∖ I ) ) )
35 32 34 jca ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o ) ∧ ( 𝑇𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇𝑦 ) ∖ I ) ) ) )
36 difeq1 ( ( 𝑇𝑦 ) = 𝐹 → ( ( 𝑇𝑦 ) ∖ I ) = ( 𝐹 ∖ I ) )
37 36 dmeqd ( ( 𝑇𝑦 ) = 𝐹 → dom ( ( 𝑇𝑦 ) ∖ I ) = dom ( 𝐹 ∖ I ) )
38 37 3 eqtr4di ( ( 𝑇𝑦 ) = 𝐹 → dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 )
39 sseq1 ( dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 → ( dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷𝑃𝐷 ) )
40 breq1 ( dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 → ( dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o𝑃 ≈ 2o ) )
41 39 40 3anbi23d ( dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 → ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o ) ↔ ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ) )
42 41 adantl ( ( ( 𝑇𝑦 ) = 𝐹 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 ) → ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o ) ↔ ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ) )
43 simpl ( ( ( 𝑇𝑦 ) = 𝐹 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 ) → ( 𝑇𝑦 ) = 𝐹 )
44 fveq2 ( dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 → ( 𝑇 ‘ dom ( ( 𝑇𝑦 ) ∖ I ) ) = ( 𝑇𝑃 ) )
45 44 adantl ( ( ( 𝑇𝑦 ) = 𝐹 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 ) → ( 𝑇 ‘ dom ( ( 𝑇𝑦 ) ∖ I ) ) = ( 𝑇𝑃 ) )
46 43 45 eqeq12d ( ( ( 𝑇𝑦 ) = 𝐹 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 ) → ( ( 𝑇𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇𝑦 ) ∖ I ) ) ↔ 𝐹 = ( 𝑇𝑃 ) ) )
47 42 46 anbi12d ( ( ( 𝑇𝑦 ) = 𝐹 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) = 𝑃 ) → ( ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o ) ∧ ( 𝑇𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇𝑦 ) ∖ I ) ) ) ↔ ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) )
48 38 47 mpdan ( ( 𝑇𝑦 ) = 𝐹 → ( ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇𝑦 ) ∖ I ) ≈ 2o ) ∧ ( 𝑇𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇𝑦 ) ∖ I ) ) ) ↔ ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) )
49 35 48 syl5ibcom ( ( 𝐷 ∈ V ∧ 𝑦𝐷𝑦 ≈ 2o ) → ( ( 𝑇𝑦 ) = 𝐹 → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) )
50 49 3exp ( 𝐷 ∈ V → ( 𝑦𝐷 → ( 𝑦 ≈ 2o → ( ( 𝑇𝑦 ) = 𝐹 → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) ) ) )
51 50 imp4a ( 𝐷 ∈ V → ( 𝑦𝐷 → ( ( 𝑦 ≈ 2o ∧ ( 𝑇𝑦 ) = 𝐹 ) → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) ) )
52 25 51 syl5 ( 𝐷 ∈ V → ( 𝑦 ∈ 𝒫 𝐷 → ( ( 𝑦 ≈ 2o ∧ ( 𝑇𝑦 ) = 𝐹 ) → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) ) )
53 52 rexlimdv ( 𝐷 ∈ V → ( ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇𝑦 ) = 𝐹 ) → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) )
54 24 53 sylbid ( 𝐷 ∈ V → ( 𝐹𝑅 → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) ) )
55 9 54 mpcom ( 𝐹𝑅 → ( ( 𝐷 ∈ V ∧ 𝑃𝐷𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇𝑃 ) ) )