Step | Hyp | Ref
| Expression |
1 | | simplr 767 |
. . . . . . 7
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) |
2 | | breq1 5069 |
. . . . . . . 8
⊢ (𝑦 = 𝑝 → (𝑦 ≈ 2o ↔ 𝑝 ≈
2o)) |
3 | 2 | elrab 3680 |
. . . . . . 7
⊢ (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↔ (𝑝 ∈ 𝒫 𝐷 ∧ 𝑝 ≈ 2o)) |
4 | 1, 3 | sylib 220 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → (𝑝 ∈ 𝒫 𝐷 ∧ 𝑝 ≈ 2o)) |
5 | 4 | simprd 498 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → 𝑝 ≈ 2o) |
6 | | en2 8754 |
. . . . 5
⊢ (𝑝 ≈ 2o →
∃𝑖∃𝑗 𝑝 = {𝑖, 𝑗}) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → ∃𝑖∃𝑗 𝑝 = {𝑖, 𝑗}) |
8 | 4 | simpld 497 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → 𝑝 ∈ 𝒫 𝐷) |
9 | 8 | elpwid 4550 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → 𝑝 ⊆ 𝐷) |
10 | 9 | adantr 483 |
. . . . . . . 8
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑝 ⊆ 𝐷) |
11 | | vex 3497 |
. . . . . . . . . 10
⊢ 𝑖 ∈ V |
12 | 11 | prid1 4698 |
. . . . . . . . 9
⊢ 𝑖 ∈ {𝑖, 𝑗} |
13 | | simpr 487 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑝 = {𝑖, 𝑗}) |
14 | 12, 13 | eleqtrrid 2920 |
. . . . . . . 8
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑖 ∈ 𝑝) |
15 | 10, 14 | sseldd 3968 |
. . . . . . 7
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑖 ∈ 𝐷) |
16 | | vex 3497 |
. . . . . . . . . 10
⊢ 𝑗 ∈ V |
17 | 16 | prid2 4699 |
. . . . . . . . 9
⊢ 𝑗 ∈ {𝑖, 𝑗} |
18 | 17, 13 | eleqtrrid 2920 |
. . . . . . . 8
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑗 ∈ 𝑝) |
19 | 10, 18 | sseldd 3968 |
. . . . . . 7
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑗 ∈ 𝐷) |
20 | 5 | adantr 483 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑝 ≈ 2o) |
21 | 13, 20 | eqbrtrrd 5090 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → {𝑖, 𝑗} ≈ 2o) |
22 | | pr2ne 9431 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷) → ({𝑖, 𝑗} ≈ 2o ↔ 𝑖 ≠ 𝑗)) |
23 | 22 | biimpa 479 |
. . . . . . . . 9
⊢ (((𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷) ∧ {𝑖, 𝑗} ≈ 2o) → 𝑖 ≠ 𝑗) |
24 | 15, 19, 21, 23 | syl21anc 835 |
. . . . . . . 8
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑖 ≠ 𝑗) |
25 | | simplr 767 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
26 | | simp-4l 781 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝐷 ∈ 𝑉) |
27 | | eqid 2821 |
. . . . . . . . . . . 12
⊢
(pmTrsp‘𝐷) =
(pmTrsp‘𝐷) |
28 | 27 | pmtrval 18579 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑝 ⊆ 𝐷 ∧ 𝑝 ≈ 2o) →
((pmTrsp‘𝐷)‘𝑝) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
29 | 26, 10, 20, 28 | syl3anc 1367 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → ((pmTrsp‘𝐷)‘𝑝) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
30 | 13 | fveq2d 6674 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → ((pmTrsp‘𝐷)‘𝑝) = ((pmTrsp‘𝐷)‘{𝑖, 𝑗})) |
31 | 25, 29, 30 | 3eqtr2d 2862 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑃 = ((pmTrsp‘𝐷)‘{𝑖, 𝑗})) |
32 | | trsp2cyc.c |
. . . . . . . . . 10
⊢ 𝐶 = (toCyc‘𝐷) |
33 | 32, 26, 15, 19, 24, 27 | cycpm2tr 30761 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → (𝐶‘〈“𝑖𝑗”〉) = ((pmTrsp‘𝐷)‘{𝑖, 𝑗})) |
34 | 31, 33 | eqtr4d 2859 |
. . . . . . . 8
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑃 = (𝐶‘〈“𝑖𝑗”〉)) |
35 | 24, 34 | jca 514 |
. . . . . . 7
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉))) |
36 | 15, 19, 35 | jca31 517 |
. . . . . 6
⊢
(((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ∧ 𝑝 = {𝑖, 𝑗}) → ((𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷) ∧ (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉)))) |
37 | 36 | ex 415 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → (𝑝 = {𝑖, 𝑗} → ((𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷) ∧ (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉))))) |
38 | 37 | 2eximdv 1920 |
. . . 4
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → (∃𝑖∃𝑗 𝑝 = {𝑖, 𝑗} → ∃𝑖∃𝑗((𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷) ∧ (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉))))) |
39 | 7, 38 | mpd 15 |
. . 3
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → ∃𝑖∃𝑗((𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷) ∧ (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉)))) |
40 | | r2ex 3303 |
. . 3
⊢
(∃𝑖 ∈
𝐷 ∃𝑗 ∈ 𝐷 (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉)) ↔ ∃𝑖∃𝑗((𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷) ∧ (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉)))) |
41 | 39, 40 | sylibr 236 |
. 2
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) ∧ 𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}) ∧ 𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → ∃𝑖 ∈ 𝐷 ∃𝑗 ∈ 𝐷 (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉))) |
42 | | simpr 487 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → 𝑃 ∈ 𝑇) |
43 | | trsp2cyc.t |
. . . . 5
⊢ 𝑇 = ran (pmTrsp‘𝐷) |
44 | 27 | pmtrfval 18578 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑉 → (pmTrsp‘𝐷) = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
45 | 44 | adantr 483 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → (pmTrsp‘𝐷) = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
46 | 45 | rneqd 5808 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → ran (pmTrsp‘𝐷) = ran (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
47 | 43, 46 | syl5eq 2868 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → 𝑇 = ran (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
48 | 42, 47 | eleqtrd 2915 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → 𝑃 ∈ ran (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
49 | | eqid 2821 |
. . . . 5
⊢ (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
50 | 49 | elrnmpt 5828 |
. . . 4
⊢ (𝑃 ∈ 𝑇 → (𝑃 ∈ ran (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ↔ ∃𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
51 | 50 | adantl 484 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → (𝑃 ∈ ran (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) ↔ ∃𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
52 | 48, 51 | mpbid 234 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → ∃𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o}𝑃 = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
53 | 41, 52 | r19.29a 3289 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → ∃𝑖 ∈ 𝐷 ∃𝑗 ∈ 𝐷 (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘〈“𝑖𝑗”〉))) |