| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pmtrrn.t | . . . . . . 7
⊢ 𝑇 = (pmTrsp‘𝐷) | 
| 2 |  | pmtrrn.r | . . . . . . 7
⊢ 𝑅 = ran 𝑇 | 
| 3 |  | eqid 2737 | . . . . . . 7
⊢ dom
(𝐹 ∖ I ) = dom (𝐹 ∖ I ) | 
| 4 | 1, 2, 3 | pmtrfrn 19476 | . . . . . 6
⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) ∧
𝐹 = (𝑇‘dom (𝐹 ∖ I )))) | 
| 5 | 4 | simpld 494 | . . . . 5
⊢ (𝐹 ∈ 𝑅 → (𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈
2o)) | 
| 6 | 1 | pmtrf 19473 | . . . . 5
⊢ ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
(𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷) | 
| 7 | 5, 6 | syl 17 | . . . 4
⊢ (𝐹 ∈ 𝑅 → (𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷) | 
| 8 | 4 | simprd 495 | . . . . 5
⊢ (𝐹 ∈ 𝑅 → 𝐹 = (𝑇‘dom (𝐹 ∖ I ))) | 
| 9 | 8 | feq1d 6720 | . . . 4
⊢ (𝐹 ∈ 𝑅 → (𝐹:𝐷⟶𝐷 ↔ (𝑇‘dom (𝐹 ∖ I )):𝐷⟶𝐷)) | 
| 10 | 7, 9 | mpbird 257 | . . 3
⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷⟶𝐷) | 
| 11 |  | fco 6760 | . . . 4
⊢ ((𝐹:𝐷⟶𝐷 ∧ 𝐹:𝐷⟶𝐷) → (𝐹 ∘ 𝐹):𝐷⟶𝐷) | 
| 12 | 11 | anidms 566 | . . 3
⊢ (𝐹:𝐷⟶𝐷 → (𝐹 ∘ 𝐹):𝐷⟶𝐷) | 
| 13 |  | ffn 6736 | . . 3
⊢ ((𝐹 ∘ 𝐹):𝐷⟶𝐷 → (𝐹 ∘ 𝐹) Fn 𝐷) | 
| 14 | 10, 12, 13 | 3syl 18 | . 2
⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) Fn 𝐷) | 
| 15 |  | fnresi 6697 | . . 3
⊢ ( I
↾ 𝐷) Fn 𝐷 | 
| 16 | 15 | a1i 11 | . 2
⊢ (𝐹 ∈ 𝑅 → ( I ↾ 𝐷) Fn 𝐷) | 
| 17 | 1, 2, 3 | pmtrffv 19477 | . . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) = if(𝑥 ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{𝑥}), 𝑥)) | 
| 18 |  | iftrue 4531 | . . . . . . 7
⊢ (𝑥 ∈ dom (𝐹 ∖ I ) → if(𝑥 ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{𝑥}), 𝑥) = ∪ (dom (𝐹 ∖ I ) ∖ {𝑥})) | 
| 19 | 17, 18 | sylan9eq 2797 | . . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑥) = ∪ (dom (𝐹 ∖ I ) ∖ {𝑥})) | 
| 20 | 19 | fveq2d 6910 | . . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) | 
| 21 |  | simpll 767 | . . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 𝐹 ∈ 𝑅) | 
| 22 | 5 | simp2d 1144 | . . . . . . . . 9
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ⊆ 𝐷) | 
| 23 | 22 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → dom (𝐹 ∖ I ) ⊆ 𝐷) | 
| 24 |  | 1onn 8678 | . . . . . . . . . . 11
⊢
1o ∈ ω | 
| 25 | 5 | simp3d 1145 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈
2o) | 
| 26 |  | df-2o 8507 | . . . . . . . . . . . . 13
⊢
2o = suc 1o | 
| 27 | 25, 26 | breqtrdi 5184 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈ suc
1o) | 
| 28 | 27 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → dom (𝐹 ∖ I ) ≈ suc
1o) | 
| 29 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → 𝑥 ∈ dom (𝐹 ∖ I )) | 
| 30 |  | dif1ennn 9201 | . . . . . . . . . . 11
⊢
((1o ∈ ω ∧ dom (𝐹 ∖ I ) ≈ suc 1o ∧
𝑥 ∈ dom (𝐹 ∖ I )) → (dom (𝐹 ∖ I ) ∖ {𝑥}) ≈
1o) | 
| 31 | 24, 28, 29, 30 | mp3an2i 1468 | . . . . . . . . . 10
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (dom (𝐹 ∖ I ) ∖ {𝑥}) ≈ 1o) | 
| 32 |  | en1uniel 9069 | . . . . . . . . . 10
⊢ ((dom
(𝐹 ∖ I ) ∖
{𝑥}) ≈ 1o
→ ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥})) | 
| 33 | 31, 32 | syl 17 | . . . . . . . . 9
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥})) | 
| 34 | 33 | eldifad 3963 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I )) | 
| 35 | 23, 34 | sseldd 3984 | . . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ 𝐷) | 
| 36 | 1, 2, 3 | pmtrffv 19477 | . . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}) ∈ 𝐷) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) | 
| 37 | 21, 35, 36 | syl2anc 584 | . . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥}))) | 
| 38 |  | iftrue 4531 | . . . . . . . 8
⊢ (∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ) → if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})})) | 
| 39 | 34, 38 | syl 17 | . . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})})) | 
| 40 | 25 | adantr 480 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → dom (𝐹 ∖ I ) ≈
2o) | 
| 41 |  | en2other2 10049 | . . . . . . . . 9
⊢ ((𝑥 ∈ dom (𝐹 ∖ I ) ∧ dom (𝐹 ∖ I ) ≈ 2o) →
∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) | 
| 42 | 41 | ancoms 458 | . . . . . . . 8
⊢ ((dom
(𝐹 ∖ I ) ≈
2o ∧ 𝑥
∈ dom (𝐹 ∖ I ))
→ ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) | 
| 43 | 40, 42 | sylan 580 | . . . . . . 7
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → ∪ (dom (𝐹 ∖ I ) ∖ {∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}) = 𝑥) | 
| 44 | 39, 43 | eqtrd 2777 | . . . . . 6
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → if(∪ (dom (𝐹 ∖ I ) ∖ {𝑥}) ∈ dom (𝐹 ∖ I ), ∪
(dom (𝐹 ∖ I ) ∖
{∪ (dom (𝐹 ∖ I ) ∖ {𝑥})}), ∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = 𝑥) | 
| 45 | 37, 44 | eqtrd 2777 | . . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘∪ (dom
(𝐹 ∖ I ) ∖
{𝑥})) = 𝑥) | 
| 46 | 20, 45 | eqtrd 2777 | . . . 4
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 47 | 10 | ffnd 6737 | . . . . . . . 8
⊢ (𝐹 ∈ 𝑅 → 𝐹 Fn 𝐷) | 
| 48 |  | fnelnfp 7197 | . . . . . . . 8
⊢ ((𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) | 
| 49 | 47, 48 | sylan 580 | . . . . . . 7
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) | 
| 50 | 49 | necon2bbid 2984 | . . . . . 6
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑥) = 𝑥 ↔ ¬ 𝑥 ∈ dom (𝐹 ∖ I ))) | 
| 51 | 50 | biimpar 477 | . . . . 5
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑥) = 𝑥) | 
| 52 |  | fveq2 6906 | . . . . . 6
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) | 
| 53 |  | id 22 | . . . . . 6
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘𝑥) = 𝑥) | 
| 54 | 52, 53 | eqtrd 2777 | . . . . 5
⊢ ((𝐹‘𝑥) = 𝑥 → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 55 | 51, 54 | syl 17 | . . . 4
⊢ (((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 56 | 46, 55 | pm2.61dan 813 | . . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 57 |  | fvco2 7006 | . . . 4
⊢ ((𝐹 Fn 𝐷 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (𝐹‘(𝐹‘𝑥))) | 
| 58 | 47, 57 | sylan 580 | . . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (𝐹‘(𝐹‘𝑥))) | 
| 59 |  | fvresi 7193 | . . . 4
⊢ (𝑥 ∈ 𝐷 → (( I ↾ 𝐷)‘𝑥) = 𝑥) | 
| 60 | 59 | adantl 481 | . . 3
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → (( I ↾ 𝐷)‘𝑥) = 𝑥) | 
| 61 | 56, 58, 60 | 3eqtr4d 2787 | . 2
⊢ ((𝐹 ∈ 𝑅 ∧ 𝑥 ∈ 𝐷) → ((𝐹 ∘ 𝐹)‘𝑥) = (( I ↾ 𝐷)‘𝑥)) | 
| 62 | 14, 16, 61 | eqfnfvd 7054 | 1
⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷)) |