Step | Hyp | Ref
| Expression |
1 | | pmtrrn.t |
. . . . . . 7
⊢ 𝑇 = (pmTrsp‘𝐷) |
2 | | pmtrrn.r |
. . . . . . 7
⊢ 𝑅 = ran 𝑇 |
3 | | eqid 2622 |
. . . . . . 7
⊢ dom
(𝐹 ∖ I ) = dom (𝐹 ∖ I ) |
4 | 1, 2, 3 | pmtrfrn 17878 |
. . . . . 6
⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2𝑜)
∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I )))) |
5 | 4 | simpld 475 |
. . . . 5
⊢ (𝐹 ∈ 𝑅 → (𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈
2𝑜)) |
6 | 1 | pmtrf 17875 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2𝑜)
→ (𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝐹 ∈ 𝑅 → (𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷) |
8 | 4 | simprd 479 |
. . . . 5
⊢ (𝐹 ∈ 𝑅 → 𝐹 = (𝑇‘dom (𝐹 ∖ I ))) |
9 | 8 | feq1d 6030 |
. . . 4
⊢ (𝐹 ∈ 𝑅 → (𝐹:𝐷⟶𝐷 ↔ (𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷)) |
10 | 7, 9 | mpbird 247 |
. . 3
⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷⟶𝐷) |
11 | | fco 6058 |
. . . 4
⊢ ((𝐹:𝐷⟶𝐷 ∧ 𝐹:𝐷⟶𝐷) → (𝐹 ∘ 𝐹):𝐷⟶𝐷) |
12 | 11 | anidms 677 |
. . 3
⊢ (𝐹:𝐷⟶𝐷 → (𝐹 ∘ 𝐹):𝐷⟶𝐷) |
13 | | ffn 6045 |
. . 3
⊢ ((𝐹 ∘ 𝐹):𝐷⟶𝐷 → (𝐹 ∘ 𝐹) Fn 𝐷) |
14 | 10, 12, 13 | 3syl 18 |
. 2
⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) Fn 𝐷) |
15 | | fnresi 6008 |
. . 3
⊢ ( I
↾ 𝐷) Fn 𝐷 |
16 | 15 | a1i 11 |
. 2
⊢ (𝐹 ∈ 𝑅 → ( I ↾ 𝐷) Fn 𝐷) |
17 | 1, 2, 3 | pmtrffv 17879 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) = if(𝑥 ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{𝑥}), 𝑥)) |
18 | | iftrue 4092 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐹 ∖ I ) → if(𝑥 ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{𝑥}), 𝑥) = ∪ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
19 | 17, 18 | sylan9eq 2676 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑥) = ∪ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
20 | 19 | fveq2d 6195 |
. . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) |
21 | | simpll 790 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 𝐹 ∈ 𝑅) |
22 | 5 | simp2d 1074 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ⊆ 𝐷) |
23 | 22 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → dom (𝐹 ∖ I ) ⊆ 𝐷) |
24 | | 1onn 7719 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ ω |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 1𝑜
∈ ω) |
26 | 5 | simp3d 1075 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈
2𝑜) |
27 | | df-2o 7561 |
. . . . . . . . . . . . 13
⊢
2𝑜 = suc 1𝑜 |
28 | 26, 27 | syl6breq 4694 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈ suc
1𝑜) |
29 | 28 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → dom (𝐹 ∖ I ) ≈ suc
1𝑜) |
30 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 𝑥 ∈ dom (𝐹 ∖ I )) |
31 | | dif1en 8193 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ ω ∧ dom (𝐹 ∖ I ) ≈ suc
1𝑜 ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (dom (𝐹 ∖ I ) ∖ {𝑥}) ≈
1𝑜) |
32 | 25, 29, 30, 31 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (dom (𝐹 ∖ I ) ∖ {𝑥}) ≈
1𝑜) |
33 | | en1uniel 8028 |
. . . . . . . . . 10
⊢ ((dom
(𝐹 ∖ I ) ∖
{𝑥}) ≈
1𝑜 → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
35 | 34 | eldifad 3586 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I )) |
36 | 23, 35 | sseldd 3604 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ 𝐷) |
37 | 1, 2, 3 | pmtrffv 17879 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}) ∈ 𝐷) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) |
38 | 21, 36, 37 | syl2anc 693 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) |
39 | | iftrue 4092 |
. . . . . . . 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 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → dom (𝐹 ∖ I ) ≈
2𝑜) |
42 | | en2other2 8832 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom (𝐹 ∖ I ) ∧ dom (𝐹 ∖ I ) ≈ 2𝑜)
→ ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) |
43 | 42 | ancoms 469 |
. . . . . . . 8
⊢ ((dom
(𝐹 ∖ I ) ≈
2𝑜 ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) |
44 | 41, 43 | sylan 488 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) |
45 | 40, 44 | eqtrd 2656 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = 𝑥) |
46 | 38, 45 | eqtrd 2656 |
. . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = 𝑥) |
47 | 20, 46 | eqtrd 2656 |
. . . 4
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
48 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐹:𝐷⟶𝐷 → 𝐹 Fn 𝐷) |
49 | 10, 48 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝑅 → 𝐹 Fn 𝐷) |
50 | | fnelnfp 6443 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) |
51 | 49, 50 | sylan 488 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) |
52 | 51 | necon2bbid 2837 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑥) = 𝑥 ↔ ¬ 𝑥 ∈ dom (𝐹 ∖ I ))) |
53 | 52 | biimpar 502 |
. . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑥) = 𝑥) |
54 | | fveq2 6191 |
. . . . . 6
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
55 | | id 22 |
. . . . . 6
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘𝑥) = 𝑥) |
56 | 54, 55 | eqtrd 2656 |
. . . . 5
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
57 | 53, 56 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
58 | 47, 57 | pm2.61dan 832 |
. . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝐹‘𝑥)) = 𝑥) |
59 | | fvco2 6273 |
. . . 4
⊢ ((𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (𝐹‘(𝐹‘𝑥))) |
60 | 49, 59 | sylan 488 |
. . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (𝐹‘(𝐹‘𝑥))) |
61 | | fvresi 6439 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (( I ↾ 𝐷)‘𝑥) = 𝑥) |
62 | 61 | adantl 482 |
. . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (( I ↾ 𝐷)‘𝑥) = 𝑥) |
63 | 58, 60, 62 | 3eqtr4d 2666 |
. 2
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (( I ↾ 𝐷)‘𝑥)) |
64 | 14, 16, 63 | eqfnfvd 6314 |
1
⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷)) |