Metamath Proof Explorer

Theorem pmtrrn2

Description: For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrrn.r ⊢ 𝑅 = ran 𝑇
Assertion pmtrrn2 ( 𝐹 ∈ 𝑅 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) )

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 5 simp3d ⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ≈ 2o )
7 en2 ⊢ ( dom ( 𝐹 ∖ I ) ≈ 2o → ∃ 𝑥 ∃ 𝑦 dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } )
8 6 7 syl ⊢ ( 𝐹 ∈ 𝑅 → ∃ 𝑥 ∃ 𝑦 dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } )
9 5 simp2d ⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ⊆ 𝐷 )
10 4 simprd ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) )
11 9 6 10 jca32 ⊢ ( 𝐹 ∈ 𝑅 → ( dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) ) )
12 sseq1 ⊢ ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( dom ( 𝐹 ∖ I ) ⊆ 𝐷 ↔ { 𝑥 , 𝑦 } ⊆ 𝐷 ) )
13 breq1 ⊢ ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( dom ( 𝐹 ∖ I ) ≈ 2o ↔ { 𝑥 , 𝑦 } ≈ 2o ) )
14 fveq2 ⊢ ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) )
15 14 eqeq2d ⊢ ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ↔ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) )
16 13 15 anbi12d ⊢ ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) ↔ ( { 𝑥 , 𝑦 } ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) )
17 12 16 anbi12d ⊢ ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( ( dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ( { 𝑥 , 𝑦 } ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) ) )
18 11 17 syl5ibcom ⊢ ( 𝐹 ∈ 𝑅 → ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ( { 𝑥 , 𝑦 } ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) ) )
19 vex ⊢ 𝑥 ∈ V
20 vex ⊢ 𝑦 ∈ V
21 19 20 prss ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐷 )
22 21 bicomi ⊢ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) )
23 pr2ne ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( { 𝑥 , 𝑦 } ≈ 2o ↔ 𝑥 ≠ 𝑦 ) )
24 23 el2v ⊢ ( { 𝑥 , 𝑦 } ≈ 2o ↔ 𝑥 ≠ 𝑦 )
25 24 anbi1i ⊢ ( ( { 𝑥 , 𝑦 } ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ↔ ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) )
26 22 25 anbi12i ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ( { 𝑥 , 𝑦 } ≈ 2o ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) )
27 18 26 syl6ib ⊢ ( 𝐹 ∈ 𝑅 → ( dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) ) )
28 27 2eximdv ⊢ ( 𝐹 ∈ 𝑅 → ( ∃ 𝑥 ∃ 𝑦 dom ( 𝐹 ∖ I ) = { 𝑥 , 𝑦 } → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) ) )
29 8 28 mpd ⊢ ( 𝐹 ∈ 𝑅 → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) )
30 r2ex ⊢ ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) )
31 29 30 sylibr ⊢ ( 𝐹 ∈ 𝑅 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) )