Proof of Theorem f1omvdmvd
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝑋 ∈ dom (𝐹 ∖ I )) |
| 2 | | f1ofn 6849 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴) |
| 3 | | difss 4136 |
. . . . . . . . 9
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
| 4 | | dmss 5913 |
. . . . . . . . 9
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
| 6 | | f1odm 6852 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→𝐴 → dom 𝐹 = 𝐴) |
| 7 | 5, 6 | sseqtrid 4026 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐴 → dom (𝐹 ∖ I ) ⊆ 𝐴) |
| 8 | 7 | sselda 3983 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝑋 ∈ 𝐴) |
| 9 | | fnelnfp 7197 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋)) |
| 10 | 2, 8, 9 | syl2an2r 685 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋)) |
| 11 | 1, 10 | mpbid 232 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ≠ 𝑋) |
| 12 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴–1-1→𝐴) |
| 13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝐹:𝐴–1-1→𝐴) |
| 14 | | f1of 6848 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴⟶𝐴) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝐹:𝐴⟶𝐴) |
| 16 | 15, 8 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ∈ 𝐴) |
| 17 | | f1fveq 7282 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1→𝐴 ∧ ((𝐹‘𝑋) ∈ 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘(𝐹‘𝑋)) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = 𝑋)) |
| 18 | 13, 16, 8, 17 | syl12anc 837 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → ((𝐹‘(𝐹‘𝑋)) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = 𝑋)) |
| 19 | 18 | necon3bid 2985 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → ((𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ 𝑋)) |
| 20 | 11, 19 | mpbird 257 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋)) |
| 21 | | fnelnfp 7197 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ (𝐹‘𝑋) ∈ 𝐴) → ((𝐹‘𝑋) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋))) |
| 22 | 2, 16, 21 | syl2an2r 685 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → ((𝐹‘𝑋) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋))) |
| 23 | 20, 22 | mpbird 257 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ∈ dom (𝐹 ∖ I )) |
| 24 | | eldifsn 4786 |
. 2
⊢ ((𝐹‘𝑋) ∈ (dom (𝐹 ∖ I ) ∖ {𝑋}) ↔ ((𝐹‘𝑋) ∈ dom (𝐹 ∖ I ) ∧ (𝐹‘𝑋) ≠ 𝑋)) |
| 25 | 23, 11, 24 | sylanbrc 583 |
1
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ∈ (dom (𝐹 ∖ I ) ∖ {𝑋})) |