Proof of Theorem f1omvdmvd
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝑋 ∈ dom (𝐹 ∖ I )) |
2 | | f1ofn 6051 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴) |
3 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝐹 Fn 𝐴) |
4 | | difss 3699 |
. . . . . . . . 9
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
5 | | dmss 5245 |
. . . . . . . . 9
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
7 | | f1odm 6054 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→𝐴 → dom 𝐹 = 𝐴) |
8 | 6, 7 | syl5sseq 3616 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐴 → dom (𝐹 ∖ I ) ⊆ 𝐴) |
9 | 8 | sselda 3568 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝑋 ∈ 𝐴) |
10 | | fnelnfp 6348 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋)) |
11 | 3, 9, 10 | syl2anc 691 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋)) |
12 | 1, 11 | mpbid 221 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ≠ 𝑋) |
13 | | f1of1 6049 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴–1-1→𝐴) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝐹:𝐴–1-1→𝐴) |
15 | | f1of 6050 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴⟶𝐴) |
16 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → 𝐹:𝐴⟶𝐴) |
17 | 16, 9 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ∈ 𝐴) |
18 | | f1fveq 6420 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1→𝐴 ∧ ((𝐹‘𝑋) ∈ 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘(𝐹‘𝑋)) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = 𝑋)) |
19 | 14, 17, 9, 18 | syl12anc 1316 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → ((𝐹‘(𝐹‘𝑋)) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = 𝑋)) |
20 | 19 | necon3bid 2826 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → ((𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ 𝑋)) |
21 | 12, 20 | mpbird 246 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋)) |
22 | | fnelnfp 6348 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ (𝐹‘𝑋) ∈ 𝐴) → ((𝐹‘𝑋) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋))) |
23 | 3, 17, 22 | syl2anc 691 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → ((𝐹‘𝑋) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(𝐹‘𝑋)) ≠ (𝐹‘𝑋))) |
24 | 21, 23 | mpbird 246 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ∈ dom (𝐹 ∖ I )) |
25 | | eldifsn 4260 |
. 2
⊢ ((𝐹‘𝑋) ∈ (dom (𝐹 ∖ I ) ∖ {𝑋}) ↔ ((𝐹‘𝑋) ∈ dom (𝐹 ∖ I ) ∧ (𝐹‘𝑋) ≠ 𝑋)) |
26 | 24, 12, 25 | sylanbrc 695 |
1
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑋 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑋) ∈ (dom (𝐹 ∖ I ) ∖ {𝑋})) |