Step | Hyp | Ref
| Expression |
1 | | usgrafun 25878 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
2 | | funfn 5833 |
. . . . 5
⊢ (Fun
𝐸 ↔ 𝐸 Fn dom 𝐸) |
3 | 2 | biimpi 205 |
. . . 4
⊢ (Fun
𝐸 → 𝐸 Fn dom 𝐸) |
4 | | fvelrnb 6153 |
. . . 4
⊢ (𝐸 Fn dom 𝐸 → (𝑌 ∈ ran 𝐸 ↔ ∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = 𝑌)) |
5 | 1, 3, 4 | 3syl 18 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝑌 ∈ ran 𝐸 ↔ ∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = 𝑌)) |
6 | | usgraf0 25877 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2}) |
7 | | f1f 6014 |
. . . . 5
⊢ (𝐸:dom 𝐸–1-1→{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → 𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2}) |
8 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ∧ 𝑥 ∈ dom 𝐸) → (𝐸‘𝑥) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2}) |
9 | | eleq1 2676 |
. . . . . . . 8
⊢ ((𝐸‘𝑥) = 𝑌 → ((𝐸‘𝑥) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ↔ 𝑌 ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2})) |
10 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → (#‘𝑦) = (#‘𝑌)) |
11 | 10 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → ((#‘𝑦) = 2 ↔ (#‘𝑌) = 2)) |
12 | 11 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑌 ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ↔ (𝑌 ∈ 𝒫 𝑉 ∧ (#‘𝑌) = 2)) |
13 | | hash2prde 13109 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝒫 𝑉 ∧ (#‘𝑌) = 2) → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})) |
14 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 = {𝑎, 𝑏} → (𝑌 ∈ 𝒫 𝑉 ↔ {𝑎, 𝑏} ∈ 𝒫 𝑉)) |
15 | | prex 4836 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑎, 𝑏} ∈ V |
16 | 15 | elpw 4114 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑎, 𝑏} ∈ 𝒫 𝑉 ↔ {𝑎, 𝑏} ⊆ 𝑉) |
17 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑎 ∈ V |
18 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑏 ∈ V |
19 | 17, 18 | prss 4291 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ↔ {𝑎, 𝑏} ⊆ 𝑉) |
20 | 16, 19 | sylbb2 227 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑎, 𝑏} ∈ 𝒫 𝑉 → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
21 | 14, 20 | syl6bi 242 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 = {𝑎, 𝑏} → (𝑌 ∈ 𝒫 𝑉 → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉))) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}) → (𝑌 ∈ 𝒫 𝑉 → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉))) |
23 | 22 | imdistanri 723 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ 𝒫 𝑉 ∧ (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
24 | 23 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝒫 𝑉 → ((𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})))) |
25 | 24 | 2eximdv 1835 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ 𝒫 𝑉 → (∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}) → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})))) |
26 | | r2ex 3043 |
. . . . . . . . . . . 12
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}) ↔ ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
27 | 25, 26 | syl6ibr 241 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ 𝒫 𝑉 → (∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
28 | 27 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝒫 𝑉 ∧ (#‘𝑌) = 2) → (∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
29 | 13, 28 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝒫 𝑉 ∧ (#‘𝑌) = 2) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})) |
30 | 12, 29 | sylbi 206 |
. . . . . . . 8
⊢ (𝑌 ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})) |
31 | 9, 30 | syl6bi 242 |
. . . . . . 7
⊢ ((𝐸‘𝑥) = 𝑌 → ((𝐸‘𝑥) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
32 | 8, 31 | syl5com 31 |
. . . . . 6
⊢ ((𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ∧ 𝑥 ∈ dom 𝐸) → ((𝐸‘𝑥) = 𝑌 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
33 | 32 | ex 449 |
. . . . 5
⊢ (𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → (𝑥 ∈ dom 𝐸 → ((𝐸‘𝑥) = 𝑌 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})))) |
34 | 6, 7, 33 | 3syl 18 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑥 ∈ dom 𝐸 → ((𝐸‘𝑥) = 𝑌 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})))) |
35 | 34 | rexlimdv 3012 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = 𝑌 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
36 | 5, 35 | sylbid 229 |
. 2
⊢ (𝑉 USGrph 𝐸 → (𝑌 ∈ ran 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))) |
37 | 36 | imp 444 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑌 ∈ ran 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏})) |