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 dif1ennn ⊢ ( ( 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 ) ) ) → 𝐹 = 𝐺 )