Proof of Theorem pmtrrn2
Step | Hyp | Ref
| Expression |
1 | | pmtrrn.t |
. . . . . . 7
⊢ 𝑇 = (pmTrsp‘𝐷) |
2 | | pmtrrn.r |
. . . . . . 7
⊢ 𝑅 = ran 𝑇 |
3 | | eqid 2610 |
. . . . . . 7
⊢ dom
(𝐹 ∖ I ) = dom (𝐹 ∖ I ) |
4 | 1, 2, 3 | pmtrfrn 17701 |
. . . . . 6
⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2𝑜)
∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I )))) |
5 | 4 | simpld 474 |
. . . . 5
⊢ (𝐹 ∈ 𝑅 → (𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈
2𝑜)) |
6 | 5 | simp3d 1068 |
. . . 4
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈
2𝑜) |
7 | | en2 8081 |
. . . 4
⊢ (dom
(𝐹 ∖ I ) ≈
2𝑜 → ∃𝑥∃𝑦dom (𝐹 ∖ I ) = {𝑥, 𝑦}) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝐹 ∈ 𝑅 → ∃𝑥∃𝑦dom (𝐹 ∖ I ) = {𝑥, 𝑦}) |
9 | 5 | simp2d 1067 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ⊆ 𝐷) |
10 | 4 | simprd 478 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑅 → 𝐹 = (𝑇‘dom (𝐹 ∖ I ))) |
11 | 9, 6, 10 | jca32 556 |
. . . . . 6
⊢ (𝐹 ∈ 𝑅 → (dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I ))))) |
12 | | sseq1 3589 |
. . . . . . 7
⊢ (dom
(𝐹 ∖ I ) = {𝑥, 𝑦} → (dom (𝐹 ∖ I ) ⊆ 𝐷 ↔ {𝑥, 𝑦} ⊆ 𝐷)) |
13 | | breq1 4586 |
. . . . . . . 8
⊢ (dom
(𝐹 ∖ I ) = {𝑥, 𝑦} → (dom (𝐹 ∖ I ) ≈ 2𝑜
↔ {𝑥, 𝑦} ≈
2𝑜)) |
14 | | fveq2 6103 |
. . . . . . . . 9
⊢ (dom
(𝐹 ∖ I ) = {𝑥, 𝑦} → (𝑇‘dom (𝐹 ∖ I )) = (𝑇‘{𝑥, 𝑦})) |
15 | 14 | eqeq2d 2620 |
. . . . . . . 8
⊢ (dom
(𝐹 ∖ I ) = {𝑥, 𝑦} → (𝐹 = (𝑇‘dom (𝐹 ∖ I )) ↔ 𝐹 = (𝑇‘{𝑥, 𝑦}))) |
16 | 13, 15 | anbi12d 743 |
. . . . . . 7
⊢ (dom
(𝐹 ∖ I ) = {𝑥, 𝑦} → ((dom (𝐹 ∖ I ) ≈ 2𝑜
∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I ))) ↔ ({𝑥, 𝑦} ≈ 2𝑜 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))) |
17 | 12, 16 | anbi12d 743 |
. . . . . 6
⊢ (dom
(𝐹 ∖ I ) = {𝑥, 𝑦} → ((dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I )))) ↔ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ({𝑥, 𝑦} ≈ 2𝑜 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))) |
18 | 11, 17 | syl5ibcom 234 |
. . . . 5
⊢ (𝐹 ∈ 𝑅 → (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ({𝑥, 𝑦} ⊆ 𝐷 ∧ ({𝑥, 𝑦} ≈ 2𝑜 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))) |
19 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
20 | | vex 3176 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
21 | 19, 20 | prss 4291 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ {𝑥, 𝑦} ⊆ 𝐷) |
22 | 21 | bicomi 213 |
. . . . . 6
⊢ ({𝑥, 𝑦} ⊆ 𝐷 ↔ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) |
23 | | pr2ne 8711 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ({𝑥, 𝑦} ≈ 2𝑜 ↔ 𝑥 ≠ 𝑦)) |
24 | 19, 20, 23 | mp2an 704 |
. . . . . . 7
⊢ ({𝑥, 𝑦} ≈ 2𝑜 ↔ 𝑥 ≠ 𝑦) |
25 | 24 | anbi1i 727 |
. . . . . 6
⊢ (({𝑥, 𝑦} ≈ 2𝑜 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})) ↔ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) |
26 | 22, 25 | anbi12i 729 |
. . . . 5
⊢ (({𝑥, 𝑦} ⊆ 𝐷 ∧ ({𝑥, 𝑦} ≈ 2𝑜 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))) |
27 | 18, 26 | syl6ib 240 |
. . . 4
⊢ (𝐹 ∈ 𝑅 → (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))) |
28 | 27 | 2eximdv 1835 |
. . 3
⊢ (𝐹 ∈ 𝑅 → (∃𝑥∃𝑦dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ∃𝑥∃𝑦((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))) |
29 | 8, 28 | mpd 15 |
. 2
⊢ (𝐹 ∈ 𝑅 → ∃𝑥∃𝑦((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))) |
30 | | r2ex 3043 |
. 2
⊢
(∃𝑥 ∈
𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))) |
31 | 29, 30 | sylibr 223 |
1
⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) |