Proof of Theorem pmtrfb
Step | Hyp | Ref
| Expression |
1 | | pmtrrn.t |
. . . . 5
⊢ 𝑇 = (pmTrsp‘𝐷) |
2 | | pmtrrn.r |
. . . . 5
⊢ 𝑅 = ran 𝑇 |
3 | | eqid 2737 |
. . . . 5
⊢ dom
(𝐹 ∖ I ) = dom (𝐹 ∖ I ) |
4 | 1, 2, 3 | pmtrfrn 18850 |
. . . 4
⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) ∧
𝐹 = (𝑇‘dom (𝐹 ∖ I )))) |
5 | | simpl1 1193 |
. . . 4
⊢ (((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) ∧
𝐹 = (𝑇‘dom (𝐹 ∖ I ))) → 𝐷 ∈ V) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐹 ∈ 𝑅 → 𝐷 ∈ V) |
7 | 1, 2 | pmtrff1o 18855 |
. . 3
⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷) |
8 | | simpl3 1195 |
. . . 4
⊢ (((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) ∧
𝐹 = (𝑇‘dom (𝐹 ∖ I ))) → dom (𝐹 ∖ I ) ≈
2o) |
9 | 4, 8 | syl 17 |
. . 3
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈
2o) |
10 | 6, 7, 9 | 3jca 1130 |
. 2
⊢ (𝐹 ∈ 𝑅 → (𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈
2o)) |
11 | | simp2 1139 |
. . . 4
⊢ ((𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
𝐹:𝐷–1-1-onto→𝐷) |
12 | | difss 4046 |
. . . . . . . 8
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
13 | | dmss 5771 |
. . . . . . . 8
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
14 | 12, 13 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
15 | | f1odm 6665 |
. . . . . . 7
⊢ (𝐹:𝐷–1-1-onto→𝐷 → dom 𝐹 = 𝐷) |
16 | 14, 15 | sseqtrid 3953 |
. . . . . 6
⊢ (𝐹:𝐷–1-1-onto→𝐷 → dom (𝐹 ∖ I ) ⊆ 𝐷) |
17 | 1, 2 | pmtrrn 18849 |
. . . . . 6
⊢ ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
(𝑇‘dom (𝐹 ∖ I )) ∈ 𝑅) |
18 | 16, 17 | syl3an2 1166 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
(𝑇‘dom (𝐹 ∖ I )) ∈ 𝑅) |
19 | 1, 2 | pmtrff1o 18855 |
. . . . 5
⊢ ((𝑇‘dom (𝐹 ∖ I )) ∈ 𝑅 → (𝑇‘dom (𝐹 ∖ I )):𝐷–1-1-onto→𝐷) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
(𝑇‘dom (𝐹 ∖ I )):𝐷–1-1-onto→𝐷) |
21 | | simp3 1140 |
. . . 4
⊢ ((𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
dom (𝐹 ∖ I ) ≈
2o) |
22 | 1 | pmtrmvd 18848 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
dom ((𝑇‘dom (𝐹 ∖ I )) ∖ I ) = dom
(𝐹 ∖ I
)) |
23 | 16, 22 | syl3an2 1166 |
. . . 4
⊢ ((𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
dom ((𝑇‘dom (𝐹 ∖ I )) ∖ I ) = dom
(𝐹 ∖ I
)) |
24 | | f1otrspeq 18839 |
. . . 4
⊢ (((𝐹:𝐷–1-1-onto→𝐷 ∧ (𝑇‘dom (𝐹 ∖ I )):𝐷–1-1-onto→𝐷) ∧ (dom (𝐹 ∖ I ) ≈ 2o ∧ dom
((𝑇‘dom (𝐹 ∖ I )) ∖ I ) = dom
(𝐹 ∖ I ))) →
𝐹 = (𝑇‘dom (𝐹 ∖ I ))) |
25 | 11, 20, 21, 23, 24 | syl22anc 839 |
. . 3
⊢ ((𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
𝐹 = (𝑇‘dom (𝐹 ∖ I ))) |
26 | 25, 18 | eqeltrd 2838 |
. 2
⊢ ((𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) →
𝐹 ∈ 𝑅) |
27 | 10, 26 | impbii 212 |
1
⊢ (𝐹 ∈ 𝑅 ↔ (𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈
2o)) |