Metamath Proof Explorer

Theorem f1omvdmvd

Description: A permutation of any class moves a point which is moved to a different point which is moved. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion f1omvdmvd ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → 𝑋 ∈ dom ( 𝐹 ∖ I ) )
2 f1ofn ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 Fn 𝐴 )
3 difss ⊢ ( 𝐹 ∖ I ) ⊆ 𝐹
4 dmss ⊢ ( ( 𝐹 ∖ I ) ⊆ 𝐹 → dom ( 𝐹 ∖ I ) ⊆ dom 𝐹 )
5 3 4 ax-mp ⊢ dom ( 𝐹 ∖ I ) ⊆ dom 𝐹
6 f1odm ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → dom 𝐹 = 𝐴 )
7 5 6 sseqtrid ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → dom ( 𝐹 ∖ I ) ⊆ 𝐴 )
8 7 sselda ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → 𝑋 ∈ 𝐴 )
9 fnelnfp ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )
10 2 8 9 syl2an2r ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )
11 1 10 mpbid ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 )
12 f1of1 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 –1-1→ 𝐴 )
13 12 adantr ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → 𝐹 : 𝐴 –1-1→ 𝐴 )
14 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 ⟶ 𝐴 )
15 14 adantr ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → 𝐹 : 𝐴 ⟶ 𝐴 )
16 15 8 ffvelrnd ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐴 )
17 f1fveq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐴 ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
18 13 16 8 17 syl12anc ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
19 18 necon3bid ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )
20 11 19 mpbird ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ ( 𝐹 ‘ 𝑋 ) )
21 fnelnfp ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
22 2 16 21 syl2an2r ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( ( 𝐹 ‘ 𝑋 ) ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
23 20 22 mpbird ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑋 ) ∈ dom ( 𝐹 ∖ I ) )
24 eldifsn ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑋 } ) ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ dom ( 𝐹 ∖ I ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )
25 23 11 24 sylanbrc ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑋 } ) )