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 syl5eq ⊢ ( ¬ 𝐷 ∈ 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 ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) )