Proof of Theorem elss2prb
Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . 4
⊢ (𝑧 = 𝑃 → (#‘𝑧) = (#‘𝑃)) |
2 | 1 | eqeq1d 2612 |
. . 3
⊢ (𝑧 = 𝑃 → ((#‘𝑧) = 2 ↔ (#‘𝑃) = 2)) |
3 | 2 | elrab 3331 |
. 2
⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (#‘𝑧) = 2} ↔ (𝑃 ∈ 𝒫 𝑉 ∧ (#‘𝑃) = 2)) |
4 | | hash2prb 13111 |
. . . . 5
⊢ (𝑃 ∈ 𝒫 𝑉 → ((#‘𝑃) = 2 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
5 | | elpwi 4117 |
. . . . . . 7
⊢ (𝑃 ∈ 𝒫 𝑉 → 𝑃 ⊆ 𝑉) |
6 | | ssrexv 3630 |
. . . . . . 7
⊢ (𝑃 ⊆ 𝑉 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝑃 ∈ 𝒫 𝑉 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
8 | | ssrexv 3630 |
. . . . . . . 8
⊢ (𝑃 ⊆ 𝑉 → (∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
9 | 5, 8 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ 𝒫 𝑉 → (∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
10 | 9 | reximdv 2999 |
. . . . . 6
⊢ (𝑃 ∈ 𝒫 𝑉 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
11 | 7, 10 | syld 46 |
. . . . 5
⊢ (𝑃 ∈ 𝒫 𝑉 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
12 | 4, 11 | sylbid 229 |
. . . 4
⊢ (𝑃 ∈ 𝒫 𝑉 → ((#‘𝑃) = 2 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))) |
13 | 12 | imp 444 |
. . 3
⊢ ((𝑃 ∈ 𝒫 𝑉 ∧ (#‘𝑃) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) |
14 | | prelpwi 4842 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → {𝑥, 𝑦} ∈ 𝒫 𝑉) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) → {𝑥, 𝑦} ∈ 𝒫 𝑉) |
16 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑃 = {𝑥, 𝑦} → (𝑃 ∈ 𝒫 𝑉 ↔ {𝑥, 𝑦} ∈ 𝒫 𝑉)) |
17 | 16 | ad2antll 761 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) → (𝑃 ∈ 𝒫 𝑉 ↔ {𝑥, 𝑦} ∈ 𝒫 𝑉)) |
18 | 15, 17 | mpbird 246 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) → 𝑃 ∈ 𝒫 𝑉) |
19 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑃 = {𝑥, 𝑦} → (#‘𝑃) = (#‘{𝑥, 𝑦})) |
20 | 19 | ad2antll 761 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) → (#‘𝑃) = (#‘{𝑥, 𝑦})) |
21 | | hashprg 13043 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 ≠ 𝑦 ↔ (#‘{𝑥, 𝑦}) = 2)) |
22 | 21 | biimpcd 238 |
. . . . . . . . 9
⊢ (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (#‘{𝑥, 𝑦}) = 2)) |
23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (#‘{𝑥, 𝑦}) = 2)) |
24 | 23 | impcom 445 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) → (#‘{𝑥, 𝑦}) = 2) |
25 | 20, 24 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) → (#‘𝑃) = 2) |
26 | 18, 25 | jca 553 |
. . . . 5
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) → (𝑃 ∈ 𝒫 𝑉 ∧ (#‘𝑃) = 2)) |
27 | 26 | ex 449 |
. . . 4
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → (𝑃 ∈ 𝒫 𝑉 ∧ (#‘𝑃) = 2))) |
28 | 27 | rexlimivv 3018 |
. . 3
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}) → (𝑃 ∈ 𝒫 𝑉 ∧ (#‘𝑃) = 2)) |
29 | 13, 28 | impbii 198 |
. 2
⊢ ((𝑃 ∈ 𝒫 𝑉 ∧ (#‘𝑃) = 2) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) |
30 | 3, 29 | bitri 263 |
1
⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (#‘𝑧) = 2} ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) |