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 ⊢ F : A ⟶ 1-1 onto A ∧ X ∈ dom ⁡ F ∖ I → F ⁡ X ∈ dom ⁡ F ∖ I ∖ X

Proof

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