Metamath Proof Explorer


Theorem f1otrspeq

Description: A transposition is characterized by the points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion f1otrspeq ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 f1ofn ( 𝐹 : 𝐴1-1-onto𝐴𝐹 Fn 𝐴 )
2 1 ad2antrr ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐹 Fn 𝐴 )
3 f1ofn ( 𝐺 : 𝐴1-1-onto𝐴𝐺 Fn 𝐴 )
4 3 ad2antlr ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐺 Fn 𝐴 )
5 1onn 1o ∈ ω
6 simplrr ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) )
7 simplrl ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐹 ∖ I ) ≈ 2o )
8 df-2o 2o = suc 1o
9 7 8 breqtrdi ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐹 ∖ I ) ≈ suc 1o )
10 6 9 eqbrtrd ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐺 ∖ I ) ≈ suc 1o )
11 simpr ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → 𝑥 ∈ dom ( 𝐺 ∖ I ) )
12 dif1en ( ( 1o ∈ ω ∧ dom ( 𝐺 ∖ I ) ≈ suc 1o𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o )
13 5 10 11 12 mp3an2i ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o )
14 euen1b ( ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o ↔ ∃! 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) )
15 eumo ( ∃! 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) → ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) )
16 14 15 sylbi ( ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o → ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) )
17 13 16 syl ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) )
18 f1omvdmvd ( ( 𝐹 : 𝐴1-1-onto𝐴𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) )
19 18 ex ( 𝐹 : 𝐴1-1-onto𝐴 → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) → ( 𝐹𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) )
20 19 ad2antrr ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) → ( 𝐹𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) )
21 eleq2 ( dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) )
22 21 ad2antll ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) )
23 difeq1 ( dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) → ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) = ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) )
24 23 eleq2d ( dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) → ( ( 𝐹𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐹𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) )
25 24 ad2antll ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( ( 𝐹𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐹𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) )
26 20 22 25 3imtr4d ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) → ( 𝐹𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) )
27 26 imp ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) )
28 f1omvdmvd ( ( 𝐺 : 𝐴1-1-onto𝐴𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐺𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) )
29 28 ad4ant24 ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐺𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) )
30 fvex ( 𝐹𝑥 ) ∈ V
31 fvex ( 𝐺𝑥 ) ∈ V
32 30 31 pm3.2i ( ( 𝐹𝑥 ) ∈ V ∧ ( 𝐺𝑥 ) ∈ V )
33 eleq1 ( 𝑦 = ( 𝐹𝑥 ) → ( 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐹𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) )
34 eleq1 ( 𝑦 = ( 𝐺𝑥 ) → ( 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐺𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) )
35 33 34 moi ( ( ( ( 𝐹𝑥 ) ∈ V ∧ ( 𝐺𝑥 ) ∈ V ) ∧ ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( ( 𝐹𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( 𝐺𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
36 32 35 mp3an1 ( ( ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( ( 𝐹𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( 𝐺𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
37 17 27 29 36 syl12anc ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
38 37 adantlr ( ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
39 simplrr ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) )
40 39 eleq2d ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) )
41 fnelnfp ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹𝑥 ) ≠ 𝑥 ) )
42 2 41 sylan ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹𝑥 ) ≠ 𝑥 ) )
43 40 42 bitrd ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ ( 𝐹𝑥 ) ≠ 𝑥 ) )
44 43 necon2bbid ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → ( ( 𝐹𝑥 ) = 𝑥 ↔ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) )
45 44 biimpar ( ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) ∧ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹𝑥 ) = 𝑥 )
46 fnelnfp ( ( 𝐺 Fn 𝐴𝑥𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ ( 𝐺𝑥 ) ≠ 𝑥 ) )
47 4 46 sylan ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ ( 𝐺𝑥 ) ≠ 𝑥 ) )
48 47 necon2bbid ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → ( ( 𝐺𝑥 ) = 𝑥 ↔ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) )
49 48 biimpar ( ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) ∧ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐺𝑥 ) = 𝑥 )
50 45 49 eqtr4d ( ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) ∧ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
51 38 50 pm2.61dan ( ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
52 2 4 51 eqfnfvd ( ( ( 𝐹 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐹 = 𝐺 )