Step | Hyp | Ref
| Expression |
1 | | pmtrfval.t |
. . . 4
⊢ 𝑇 = (pmTrsp‘𝐷) |
2 | 1 | pmtrf 18075 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑇‘𝑃):𝐷⟶𝐷) |
3 | | ffn 6183 |
. . 3
⊢ ((𝑇‘𝑃):𝐷⟶𝐷 → (𝑇‘𝑃) Fn 𝐷) |
4 | | fndifnfp 6584 |
. . 3
⊢ ((𝑇‘𝑃) Fn 𝐷 → dom ((𝑇‘𝑃) ∖ I ) = {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧}) |
5 | 2, 3, 4 | 3syl 18 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → dom
((𝑇‘𝑃) ∖ I ) = {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧}) |
6 | 1 | pmtrfv 18072 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑧) = if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)) |
7 | 6 | neeq1d 3002 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → (((𝑇‘𝑃)‘𝑧) ≠ 𝑧 ↔ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧)) |
8 | | iffalse 4234 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = 𝑧) |
9 | 8 | necon1ai 2970 |
. . . . . . 7
⊢ (if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 → 𝑧 ∈ 𝑃) |
10 | | iftrue 4231 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = ∪ (𝑃 ∖ {𝑧})) |
11 | 10 | adantl 467 |
. . . . . . . . 9
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = ∪ (𝑃 ∖ {𝑧})) |
12 | | 1onn 7871 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ ω |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 1𝑜 ∈
ω) |
14 | | simpl3 1231 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 𝑃 ≈
2𝑜) |
15 | | df-2o 7712 |
. . . . . . . . . . . 12
⊢
2𝑜 = suc 1𝑜 |
16 | 14, 15 | syl6breq 4827 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 𝑃 ≈ suc
1𝑜) |
17 | | simpr 471 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → 𝑧 ∈ 𝑃) |
18 | | dif1en 8347 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ ω ∧ 𝑃 ≈ suc 1𝑜 ∧
𝑧 ∈ 𝑃) → (𝑃 ∖ {𝑧}) ≈
1𝑜) |
19 | 13, 16, 17, 18 | syl3anc 1476 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → (𝑃 ∖ {𝑧}) ≈
1𝑜) |
20 | | en1uniel 8179 |
. . . . . . . . . 10
⊢ ((𝑃 ∖ {𝑧}) ≈ 1𝑜 → ∪ (𝑃
∖ {𝑧}) ∈ (𝑃 ∖ {𝑧})) |
21 | | eldifsni 4457 |
. . . . . . . . . 10
⊢ (∪ (𝑃
∖ {𝑧}) ∈ (𝑃 ∖ {𝑧}) → ∪ (𝑃 ∖ {𝑧}) ≠ 𝑧) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → ∪ (𝑃 ∖ {𝑧}) ≠ 𝑧) |
23 | 11, 22 | eqnetrd 3010 |
. . . . . . . 8
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝑃) → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧) |
24 | 23 | ex 397 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧)) |
25 | 9, 24 | impbid2 216 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(if(𝑧 ∈ 𝑃, ∪
(𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃)) |
26 | 25 | adantr 466 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → (if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃)) |
27 | 7, 26 | bitrd 268 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑧 ∈ 𝐷) → (((𝑇‘𝑃)‘𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃)) |
28 | 27 | rabbidva 3338 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
{𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧} = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃}) |
29 | | incom 3956 |
. . . 4
⊢ (𝑃 ∩ 𝐷) = (𝐷 ∩ 𝑃) |
30 | | dfin5 3731 |
. . . 4
⊢ (𝐷 ∩ 𝑃) = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃} |
31 | 29, 30 | eqtri 2793 |
. . 3
⊢ (𝑃 ∩ 𝐷) = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃} |
32 | 28, 31 | syl6eqr 2823 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
{𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧} = (𝑃 ∩ 𝐷)) |
33 | | simp2 1131 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ⊆ 𝐷) |
34 | | df-ss 3737 |
. . 3
⊢ (𝑃 ⊆ 𝐷 ↔ (𝑃 ∩ 𝐷) = 𝑃) |
35 | 33, 34 | sylib 208 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑃 ∩ 𝐷) = 𝑃) |
36 | 5, 32, 35 | 3eqtrd 2809 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → dom
((𝑇‘𝑃) ∖ I ) = 𝑃) |