Proof of Theorem pmtrprfv
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝐷 ∈ 𝑉) |
2 | | simpr1 1060 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ 𝐷) |
3 | | simpr2 1061 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ 𝐷) |
4 | | prssi 4293 |
. . . 4
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷) → {𝑋, 𝑌} ⊆ 𝐷) |
5 | 2, 3, 4 | syl2anc 691 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → {𝑋, 𝑌} ⊆ 𝐷) |
6 | | pr2nelem 8710 |
. . . 4
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ≈
2𝑜) |
7 | 6 | adantl 481 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → {𝑋, 𝑌} ≈
2𝑜) |
8 | | pmtrfval.t |
. . . 4
⊢ 𝑇 = (pmTrsp‘𝐷) |
9 | 8 | pmtrfv 17695 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ {𝑋, 𝑌} ⊆ 𝐷 ∧ {𝑋, 𝑌} ≈ 2𝑜) ∧ 𝑋 ∈ 𝐷) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = if(𝑋 ∈ {𝑋, 𝑌}, ∪ ({𝑋, 𝑌} ∖ {𝑋}), 𝑋)) |
10 | 1, 5, 7, 2, 9 | syl31anc 1321 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = if(𝑋 ∈ {𝑋, 𝑌}, ∪ ({𝑋, 𝑌} ∖ {𝑋}), 𝑋)) |
11 | | prid1g 4239 |
. . . . 5
⊢ (𝑋 ∈ 𝐷 → 𝑋 ∈ {𝑋, 𝑌}) |
12 | 2, 11 | syl 17 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ {𝑋, 𝑌}) |
13 | 12 | iftrued 4044 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → if(𝑋 ∈ {𝑋, 𝑌}, ∪ ({𝑋, 𝑌} ∖ {𝑋}), 𝑋) = ∪ ({𝑋, 𝑌} ∖ {𝑋})) |
14 | | difprsnss 4270 |
. . . . . . 7
⊢ ({𝑋, 𝑌} ∖ {𝑋}) ⊆ {𝑌} |
15 | 14 | a1i 11 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ({𝑋, 𝑌} ∖ {𝑋}) ⊆ {𝑌}) |
16 | | prid2g 4240 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝐷 → 𝑌 ∈ {𝑋, 𝑌}) |
17 | 3, 16 | syl 17 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ {𝑋, 𝑌}) |
18 | | simpr3 1062 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ≠ 𝑌) |
19 | 18 | necomd 2837 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ≠ 𝑋) |
20 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝑌 ∈ ({𝑋, 𝑌} ∖ {𝑋}) ↔ (𝑌 ∈ {𝑋, 𝑌} ∧ 𝑌 ≠ 𝑋)) |
21 | 17, 19, 20 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ ({𝑋, 𝑌} ∖ {𝑋})) |
22 | 21 | snssd 4281 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → {𝑌} ⊆ ({𝑋, 𝑌} ∖ {𝑋})) |
23 | 15, 22 | eqssd 3585 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ({𝑋, 𝑌} ∖ {𝑋}) = {𝑌}) |
24 | 23 | unieqd 4382 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ∪
({𝑋, 𝑌} ∖ {𝑋}) = ∪ {𝑌}) |
25 | | unisng 4388 |
. . . . 5
⊢ (𝑌 ∈ 𝐷 → ∪ {𝑌} = 𝑌) |
26 | 3, 25 | syl 17 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ∪
{𝑌} = 𝑌) |
27 | 24, 26 | eqtrd 2644 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ∪
({𝑋, 𝑌} ∖ {𝑋}) = 𝑌) |
28 | 13, 27 | eqtrd 2644 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → if(𝑋 ∈ {𝑋, 𝑌}, ∪ ({𝑋, 𝑌} ∖ {𝑋}), 𝑋) = 𝑌) |
29 | 10, 28 | eqtrd 2644 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌) |