Step | Hyp | Ref
| Expression |
1 | | pmtrfval.t |
. . . 4
⊢ 𝑇 = (pmTrsp‘𝐷) |
2 | 1 | pmtrf 17698 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑇‘𝑃):𝐷⟶𝐷) |
3 | | ffn 5958 |
. . 3
⊢ ((𝑇‘𝑃):𝐷⟶𝐷 → (𝑇‘𝑃) Fn 𝐷) |
4 | | fndifnfp 6347 |
. . 3
⊢ ((𝑇‘𝑃) Fn 𝐷 → dom ((𝑇‘𝑃) ∖ I ) = {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧}) |
5 | 2, 3, 4 | 3syl 18 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → dom
((𝑇‘𝑃) ∖ I ) = {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧}) |
6 | 1 | pmtrfv 17695 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑧) = if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)) |
7 | 6 | neeq1d 2841 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → (((𝑇‘𝑃)‘𝑧) ≠ 𝑧 ↔ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧)) |
8 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = 𝑧) |
9 | 8 | necon1ai 2809 |
. . . . . . 7
⊢ (if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 → 𝑧 ∈ 𝑃) |
10 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = ∪ (𝑃 ∖ {𝑧})) |
11 | 10 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = ∪ (𝑃 ∖ {𝑧})) |
12 | | 1onn 7606 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ ω |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 1𝑜 ∈
ω) |
14 | | simpl3 1059 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 𝑃 ≈
2𝑜) |
15 | | df-2o 7448 |
. . . . . . . . . . . 12
⊢
2𝑜 = suc 1𝑜 |
16 | 14, 15 | syl6breq 4624 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 𝑃 ≈ suc
1𝑜) |
17 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 𝑧 ∈ 𝑃) |
18 | | dif1en 8078 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ ω ∧ 𝑃 ≈ suc 1𝑜 ∧
𝑧 ∈ 𝑃) → (𝑃 ∖ {𝑧}) ≈
1𝑜) |
19 | 13, 16, 17, 18 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → (𝑃 ∖ {𝑧}) ≈
1𝑜) |
20 | | en1uniel 7914 |
. . . . . . . . . 10
⊢ ((𝑃 ∖ {𝑧}) ≈ 1𝑜 → ∪ (𝑃
∖ {𝑧}) ∈ (𝑃 ∖ {𝑧})) |
21 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ (∪ (𝑃
∖ {𝑧}) ∈ (𝑃 ∖ {𝑧}) → ∪ (𝑃 ∖ {𝑧}) ≠ 𝑧) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → ∪ (𝑃 ∖ {𝑧}) ≠ 𝑧) |
23 | 11, 22 | eqnetrd 2849 |
. . . . . . . 8
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧) |
24 | 23 | ex 449 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧)) |
25 | 9, 24 | impbid2 215 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(if(𝑧 ∈ 𝑃, ∪
(𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃)) |
26 | 25 | adantr 480 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → (if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃)) |
27 | 7, 26 | bitrd 267 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → (((𝑇‘𝑃)‘𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃)) |
28 | 27 | rabbidva 3163 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
{𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧} = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃}) |
29 | | incom 3767 |
. . . 4
⊢ (𝑃 ∩ 𝐷) = (𝐷 ∩ 𝑃) |
30 | | dfin5 3548 |
. . . 4
⊢ (𝐷 ∩ 𝑃) = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃} |
31 | 29, 30 | eqtri 2632 |
. . 3
⊢ (𝑃 ∩ 𝐷) = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃} |
32 | 28, 31 | syl6eqr 2662 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
{𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧} = (𝑃 ∩ 𝐷)) |
33 | | simp2 1055 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ⊆ 𝐷) |
34 | | df-ss 3554 |
. . 3
⊢ (𝑃 ⊆ 𝐷 ↔ (𝑃 ∩ 𝐷) = 𝑃) |
35 | 33, 34 | sylib 207 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑃 ∩ 𝐷) = 𝑃) |
36 | 5, 32, 35 | 3eqtrd 2648 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → dom
((𝑇‘𝑃) ∖ I ) = 𝑃) |