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 ( 𝐹𝑅 → ∃ 𝑥𝐷𝑦𝐷 ( 𝑥𝑦𝐹 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) )