Step | Hyp | Ref
| Expression |
1 | | pmtrrn.t |
. . . . . . 7
⊢ 𝑇 = (pmTrsp‘𝐷) |
2 | | pmtrrn.r |
. . . . . . 7
⊢ 𝑅 = ran 𝑇 |
3 | | eqid 2825 |
. . . . . . 7
⊢ dom
(𝐹 ∖ I ) = dom (𝐹 ∖ I ) |
4 | 1, 2, 3 | pmtrfrn 18228 |
. . . . . 6
⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) ∧
𝐹 = (𝑇‘dom (𝐹 ∖ I )))) |
5 | 4 | simpld 490 |
. . . . 5
⊢ (𝐹 ∈ 𝑅 → (𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈
2o)) |
6 | 1 | pmtrf 18225 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
(𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝐹 ∈ 𝑅 → (𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷) |
8 | 4 | simprd 491 |
. . . . 5
⊢ (𝐹 ∈ 𝑅 → 𝐹 = (𝑇‘dom (𝐹 ∖ I ))) |
9 | 8 | feq1d 6263 |
. . . 4
⊢ (𝐹 ∈ 𝑅 → (𝐹:𝐷⟶𝐷 ↔ (𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷)) |
10 | 7, 9 | mpbird 249 |
. . 3
⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷⟶𝐷) |
11 | | fco 6295 |
. . . 4
⊢ ((𝐹:𝐷⟶𝐷 ∧ 𝐹:𝐷⟶𝐷) → (𝐹 ∘ 𝐹):𝐷⟶𝐷) |
12 | 11 | anidms 562 |
. . 3
⊢ (𝐹:𝐷⟶𝐷 → (𝐹 ∘ 𝐹):𝐷⟶𝐷) |
13 | | ffn 6278 |
. . 3
⊢ ((𝐹 ∘ 𝐹):𝐷⟶𝐷 → (𝐹 ∘ 𝐹) Fn 𝐷) |
14 | 10, 12, 13 | 3syl 18 |
. 2
⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) Fn 𝐷) |
15 | | fnresi 6241 |
. . 3
⊢ ( I
↾ 𝐷) Fn 𝐷 |
16 | 15 | a1i 11 |
. 2
⊢ (𝐹 ∈ 𝑅 → ( I ↾ 𝐷) Fn 𝐷) |
17 | 1, 2, 3 | pmtrffv 18229 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) = if(𝑥 ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{𝑥}), 𝑥)) |
18 | | iftrue 4312 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐹 ∖ I ) → if(𝑥 ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{𝑥}), 𝑥) = ∪ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
19 | 17, 18 | sylan9eq 2881 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑥) = ∪ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
20 | 19 | fveq2d 6437 |
. . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) |
21 | | simpll 783 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 𝐹 ∈ 𝑅) |
22 | 5 | simp2d 1177 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ⊆ 𝐷) |
23 | 22 | ad2antrr 717 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → dom (𝐹 ∖ I ) ⊆ 𝐷) |
24 | | 1onn 7986 |
. . . . . . . . . . . 12
⊢
1o ∈ ω |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 1o ∈
ω) |
26 | 5 | simp3d 1178 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈
2o) |
27 | | df-2o 7827 |
. . . . . . . . . . . . 13
⊢
2o = suc 1o |
28 | 26, 27 | syl6breq 4914 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈ suc
1o) |
29 | 28 | ad2antrr 717 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → dom (𝐹 ∖ I ) ≈ suc
1o) |
30 | | simpr 479 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 𝑥 ∈ dom (𝐹 ∖ I )) |
31 | | dif1en 8462 |
. . . . . . . . . . 11
⊢
((1o ∈ ω ∧ dom (𝐹 ∖ I ) ≈ suc 1o ∧
𝑥 ∈ dom (𝐹 ∖ I )) → (dom (𝐹 ∖ I ) ∖ {𝑥}) ≈
1o) |
32 | 25, 29, 30, 31 | syl3anc 1494 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (dom (𝐹 ∖ I ) ∖ {𝑥}) ≈ 1o) |
33 | | en1uniel 8294 |
. . . . . . . . . 10
⊢ ((dom
(𝐹 ∖ I ) ∖
{𝑥}) ≈ 1o
→ ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
35 | 34 | eldifad 3810 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I )) |
36 | 23, 35 | sseldd 3828 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ 𝐷) |
37 | 1, 2, 3 | pmtrffv 18229 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}) ∈ 𝐷) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) |
38 | 21, 36, 37 | syl2anc 579 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) |
39 | | iftrue 4312 |
. . . . . . . 8
⊢ (∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ) → if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})})) |
40 | 35, 39 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})})) |
41 | 26 | adantr 474 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → dom (𝐹 ∖ I ) ≈
2o) |
42 | | en2other2 9145 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom (𝐹 ∖ I ) ∧ dom (𝐹 ∖ I ) ≈ 2o) →
∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) |
43 | 42 | ancoms 452 |
. . . . . . . 8
⊢ ((dom
(𝐹 ∖ I ) ≈
2o ∧ 𝑥
∈ dom (𝐹 ∖ I ))
→ ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) |
44 | 41, 43 | sylan 575 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) |
45 | 40, 44 | eqtrd 2861 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = 𝑥) |
46 | 38, 45 | eqtrd 2861 |
. . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = 𝑥) |
47 | 20, 46 | eqtrd 2861 |
. . . 4
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
48 | 10 | ffnd 6279 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝑅 → 𝐹 Fn 𝐷) |
49 | | fnelnfp 6695 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) |
50 | 48, 49 | sylan 575 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) |
51 | 50 | necon2bbid 3042 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑥) = 𝑥 ↔ ¬ 𝑥 ∈ dom (𝐹 ∖ I ))) |
52 | 51 | biimpar 471 |
. . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑥) = 𝑥) |
53 | | fveq2 6433 |
. . . . . 6
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
54 | | id 22 |
. . . . . 6
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘𝑥) = 𝑥) |
55 | 53, 54 | eqtrd 2861 |
. . . . 5
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
56 | 52, 55 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
57 | 47, 56 | pm2.61dan 847 |
. . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
58 | | fvco2 6520 |
. . . 4
⊢ ((𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (𝐹‘(𝐹‘𝑥))) |
59 | 48, 58 | sylan 575 |
. . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (𝐹‘(𝐹‘𝑥))) |
60 | | fvresi 6691 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (( I ↾ 𝐷)‘𝑥) = 𝑥) |
61 | 60 | adantl 475 |
. . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (( I ↾ 𝐷)‘𝑥) = 𝑥) |
62 | 57, 59, 61 | 3eqtr4d 2871 |
. 2
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (( I ↾ 𝐷)‘𝑥)) |
63 | 14, 16, 62 | eqfnfvd 6563 |
1
⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷)) |