Step | Hyp | Ref
| Expression |
1 | | noel 3878 |
. . . 4
⊢ ¬
𝐹 ∈
∅ |
2 | | pmtrrn.r |
. . . . . 6
⊢ 𝑅 = ran 𝑇 |
3 | | pmtrrn.t |
. . . . . . . . 9
⊢ 𝑇 = (pmTrsp‘𝐷) |
4 | | fvprc 6097 |
. . . . . . . . 9
⊢ (¬
𝐷 ∈ V →
(pmTrsp‘𝐷) =
∅) |
5 | 3, 4 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
𝐷 ∈ V → 𝑇 = ∅) |
6 | 5 | rneqd 5274 |
. . . . . . 7
⊢ (¬
𝐷 ∈ V → ran 𝑇 = ran ∅) |
7 | | rn0 5298 |
. . . . . . 7
⊢ ran
∅ = ∅ |
8 | 6, 7 | syl6eq 2660 |
. . . . . 6
⊢ (¬
𝐷 ∈ V → ran 𝑇 = ∅) |
9 | 2, 8 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝐷 ∈ V → 𝑅 = ∅) |
10 | 9 | eleq2d 2673 |
. . . 4
⊢ (¬
𝐷 ∈ V → (𝐹 ∈ 𝑅 ↔ 𝐹 ∈ ∅)) |
11 | 1, 10 | mtbiri 316 |
. . 3
⊢ (¬
𝐷 ∈ V → ¬
𝐹 ∈ 𝑅) |
12 | 11 | con4i 112 |
. 2
⊢ (𝐹 ∈ 𝑅 → 𝐷 ∈ V) |
13 | | mptexg 6389 |
. . . . . . . 8
⊢ (𝐷 ∈ V → (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧)) ∈ V) |
14 | 13 | ralrimivw 2950 |
. . . . . . 7
⊢ (𝐷 ∈ V → ∀𝑤 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧)) ∈ V) |
15 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧))) = (𝑤 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧))) |
16 | 15 | fnmpt 5933 |
. . . . . . 7
⊢
(∀𝑤 ∈
{𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧)) ∈ V → (𝑤 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧))) Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜}) |
17 | 14, 16 | syl 17 |
. . . . . 6
⊢ (𝐷 ∈ V → (𝑤 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧))) Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜}) |
18 | 3 | pmtrfval 17693 |
. . . . . . 7
⊢ (𝐷 ∈ V → 𝑇 = (𝑤 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧)))) |
19 | 18 | fneq1d 5895 |
. . . . . 6
⊢ (𝐷 ∈ V → (𝑇 Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↔ (𝑤 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑤, ∪ (𝑤 ∖ {𝑧}), 𝑧))) Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜})) |
20 | 17, 19 | mpbird 246 |
. . . . 5
⊢ (𝐷 ∈ V → 𝑇 Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜}) |
21 | | fvelrnb 6153 |
. . . . 5
⊢ (𝑇 Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} → (𝐹 ∈ ran 𝑇 ↔ ∃𝑦 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑇‘𝑦) = 𝐹)) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ (𝐷 ∈ V → (𝐹 ∈ ran 𝑇 ↔ ∃𝑦 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑇‘𝑦) = 𝐹)) |
23 | 2 | eleq2i 2680 |
. . . 4
⊢ (𝐹 ∈ 𝑅 ↔ 𝐹 ∈ ran 𝑇) |
24 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 2𝑜 ↔ 𝑦 ≈
2𝑜)) |
25 | 24 | rexrab 3337 |
. . . . 5
⊢
(∃𝑦 ∈
{𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑇‘𝑦) = 𝐹 ↔ ∃𝑦 ∈ 𝒫 𝐷(𝑦 ≈ 2𝑜 ∧ (𝑇‘𝑦) = 𝐹)) |
26 | 25 | bicomi 213 |
. . . 4
⊢
(∃𝑦 ∈
𝒫 𝐷(𝑦 ≈ 2𝑜
∧ (𝑇‘𝑦) = 𝐹) ↔ ∃𝑦 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑇‘𝑦) = 𝐹) |
27 | 22, 23, 26 | 3bitr4g 302 |
. . 3
⊢ (𝐷 ∈ V → (𝐹 ∈ 𝑅 ↔ ∃𝑦 ∈ 𝒫 𝐷(𝑦 ≈ 2𝑜 ∧ (𝑇‘𝑦) = 𝐹))) |
28 | | elpwi 4117 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 𝐷 → 𝑦 ⊆ 𝐷) |
29 | | simp1 1054 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → 𝐷 ∈ V) |
30 | 3 | pmtrmvd 17699 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → dom
((𝑇‘𝑦) ∖ I ) = 𝑦) |
31 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → 𝑦 ⊆ 𝐷) |
32 | 30, 31 | eqsstrd 3602 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → dom
((𝑇‘𝑦) ∖ I ) ⊆ 𝐷) |
33 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → 𝑦 ≈
2𝑜) |
34 | 30, 33 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → dom
((𝑇‘𝑦) ∖ I ) ≈
2𝑜) |
35 | 29, 32, 34 | 3jca 1235 |
. . . . . . . . 9
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → (𝐷 ∈ V ∧ dom ((𝑇‘𝑦) ∖ I ) ⊆ 𝐷 ∧ dom ((𝑇‘𝑦) ∖ I ) ≈
2𝑜)) |
36 | 30 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → 𝑦 = dom ((𝑇‘𝑦) ∖ I )) |
37 | 36 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) → (𝑇‘𝑦) = (𝑇‘dom ((𝑇‘𝑦) ∖ I ))) |
38 | 35, 37 | jca 553 |
. . . . . . . 8
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) →
((𝐷 ∈ V ∧ dom
((𝑇‘𝑦) ∖ I ) ⊆ 𝐷 ∧ dom ((𝑇‘𝑦) ∖ I ) ≈ 2𝑜)
∧ (𝑇‘𝑦) = (𝑇‘dom ((𝑇‘𝑦) ∖ I )))) |
39 | | difeq1 3683 |
. . . . . . . . . . 11
⊢ ((𝑇‘𝑦) = 𝐹 → ((𝑇‘𝑦) ∖ I ) = (𝐹 ∖ I )) |
40 | 39 | dmeqd 5248 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑦) = 𝐹 → dom ((𝑇‘𝑦) ∖ I ) = dom (𝐹 ∖ I )) |
41 | | pmtrfrn.p |
. . . . . . . . . 10
⊢ 𝑃 = dom (𝐹 ∖ I ) |
42 | 40, 41 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑇‘𝑦) = 𝐹 → dom ((𝑇‘𝑦) ∖ I ) = 𝑃) |
43 | | sseq1 3589 |
. . . . . . . . . . . 12
⊢ (dom
((𝑇‘𝑦) ∖ I ) = 𝑃 → (dom ((𝑇‘𝑦) ∖ I ) ⊆ 𝐷 ↔ 𝑃 ⊆ 𝐷)) |
44 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (dom
((𝑇‘𝑦) ∖ I ) = 𝑃 → (dom ((𝑇‘𝑦) ∖ I ) ≈ 2𝑜
↔ 𝑃 ≈
2𝑜)) |
45 | 43, 44 | 3anbi23d 1394 |
. . . . . . . . . . 11
⊢ (dom
((𝑇‘𝑦) ∖ I ) = 𝑃 → ((𝐷 ∈ V ∧ dom ((𝑇‘𝑦) ∖ I ) ⊆ 𝐷 ∧ dom ((𝑇‘𝑦) ∖ I ) ≈ 2𝑜)
↔ (𝐷 ∈ V ∧
𝑃 ⊆ 𝐷 ∧ 𝑃 ≈
2𝑜))) |
46 | 45 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑇‘𝑦) = 𝐹 ∧ dom ((𝑇‘𝑦) ∖ I ) = 𝑃) → ((𝐷 ∈ V ∧ dom ((𝑇‘𝑦) ∖ I ) ⊆ 𝐷 ∧ dom ((𝑇‘𝑦) ∖ I ) ≈ 2𝑜)
↔ (𝐷 ∈ V ∧
𝑃 ⊆ 𝐷 ∧ 𝑃 ≈
2𝑜))) |
47 | | simpl 472 |
. . . . . . . . . . 11
⊢ (((𝑇‘𝑦) = 𝐹 ∧ dom ((𝑇‘𝑦) ∖ I ) = 𝑃) → (𝑇‘𝑦) = 𝐹) |
48 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (dom
((𝑇‘𝑦) ∖ I ) = 𝑃 → (𝑇‘dom ((𝑇‘𝑦) ∖ I )) = (𝑇‘𝑃)) |
49 | 48 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑇‘𝑦) = 𝐹 ∧ dom ((𝑇‘𝑦) ∖ I ) = 𝑃) → (𝑇‘dom ((𝑇‘𝑦) ∖ I )) = (𝑇‘𝑃)) |
50 | 47, 49 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (((𝑇‘𝑦) = 𝐹 ∧ dom ((𝑇‘𝑦) ∖ I ) = 𝑃) → ((𝑇‘𝑦) = (𝑇‘dom ((𝑇‘𝑦) ∖ I )) ↔ 𝐹 = (𝑇‘𝑃))) |
51 | 46, 50 | anbi12d 743 |
. . . . . . . . 9
⊢ (((𝑇‘𝑦) = 𝐹 ∧ dom ((𝑇‘𝑦) ∖ I ) = 𝑃) → (((𝐷 ∈ V ∧ dom ((𝑇‘𝑦) ∖ I ) ⊆ 𝐷 ∧ dom ((𝑇‘𝑦) ∖ I ) ≈ 2𝑜)
∧ (𝑇‘𝑦) = (𝑇‘dom ((𝑇‘𝑦) ∖ I ))) ↔ ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃)))) |
52 | 42, 51 | mpdan 699 |
. . . . . . . 8
⊢ ((𝑇‘𝑦) = 𝐹 → (((𝐷 ∈ V ∧ dom ((𝑇‘𝑦) ∖ I ) ⊆ 𝐷 ∧ dom ((𝑇‘𝑦) ∖ I ) ≈ 2𝑜)
∧ (𝑇‘𝑦) = (𝑇‘dom ((𝑇‘𝑦) ∖ I ))) ↔ ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃)))) |
53 | 38, 52 | syl5ibcom 234 |
. . . . . . 7
⊢ ((𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2𝑜) →
((𝑇‘𝑦) = 𝐹 → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃)))) |
54 | 53 | 3exp 1256 |
. . . . . 6
⊢ (𝐷 ∈ V → (𝑦 ⊆ 𝐷 → (𝑦 ≈ 2𝑜 → ((𝑇‘𝑦) = 𝐹 → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃)))))) |
55 | 54 | imp4a 612 |
. . . . 5
⊢ (𝐷 ∈ V → (𝑦 ⊆ 𝐷 → ((𝑦 ≈ 2𝑜 ∧ (𝑇‘𝑦) = 𝐹) → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃))))) |
56 | 28, 55 | syl5 33 |
. . . 4
⊢ (𝐷 ∈ V → (𝑦 ∈ 𝒫 𝐷 → ((𝑦 ≈ 2𝑜 ∧ (𝑇‘𝑦) = 𝐹) → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃))))) |
57 | 56 | rexlimdv 3012 |
. . 3
⊢ (𝐷 ∈ V → (∃𝑦 ∈ 𝒫 𝐷(𝑦 ≈ 2𝑜 ∧ (𝑇‘𝑦) = 𝐹) → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃)))) |
58 | 27, 57 | sylbid 229 |
. 2
⊢ (𝐷 ∈ V → (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃)))) |
59 | 12, 58 | mpcom 37 |
1
⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃))) |