Proof of Theorem lfuhgr3
Step | Hyp | Ref
| Expression |
1 | | lfuhgr3.1 |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | lfuhgr3.2 |
. . 3
⊢ 𝐼 = (iEdg‘𝐺) |
3 | 1, 2 | lfuhgr2 32747 |
. 2
⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)(♯‘𝑥) ≠ 1)) |
4 | | df-ne 2933 |
. . . . 5
⊢
((♯‘𝑥)
≠ 1 ↔ ¬ (♯‘𝑥) = 1) |
5 | 4 | ralbii 3078 |
. . . 4
⊢
(∀𝑥 ∈
(Edg‘𝐺)(♯‘𝑥) ≠ 1 ↔ ∀𝑥 ∈ (Edg‘𝐺) ¬ (♯‘𝑥) = 1) |
6 | | ralnex 3148 |
. . . 4
⊢
(∀𝑥 ∈
(Edg‘𝐺) ¬
(♯‘𝑥) = 1
↔ ¬ ∃𝑥
∈ (Edg‘𝐺)(♯‘𝑥) = 1) |
7 | | df-rex 3057 |
. . . . 5
⊢
(∃𝑥 ∈
(Edg‘𝐺)(♯‘𝑥) = 1 ↔ ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ (♯‘𝑥) = 1)) |
8 | 7 | notbii 323 |
. . . 4
⊢ (¬
∃𝑥 ∈
(Edg‘𝐺)(♯‘𝑥) = 1 ↔ ¬ ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ (♯‘𝑥) = 1)) |
9 | 5, 6, 8 | 3bitri 300 |
. . 3
⊢
(∀𝑥 ∈
(Edg‘𝐺)(♯‘𝑥) ≠ 1 ↔ ¬ ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ (♯‘𝑥) = 1)) |
10 | | hashen1 13902 |
. . . . . . . 8
⊢ (𝑥 ∈ V →
((♯‘𝑥) = 1
↔ 𝑥 ≈
1o)) |
11 | 10 | elv 3404 |
. . . . . . 7
⊢
((♯‘𝑥) =
1 ↔ 𝑥 ≈
1o) |
12 | | en1 8676 |
. . . . . . 7
⊢ (𝑥 ≈ 1o ↔
∃𝑎 𝑥 = {𝑎}) |
13 | 11, 12 | bitri 278 |
. . . . . 6
⊢
((♯‘𝑥) =
1 ↔ ∃𝑎 𝑥 = {𝑎}) |
14 | 13 | anbi2i 626 |
. . . . 5
⊢ ((𝑥 ∈ (Edg‘𝐺) ∧ (♯‘𝑥) = 1) ↔ (𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
15 | 14 | exbii 1855 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ (♯‘𝑥) = 1) ↔ ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
16 | 15 | notbii 323 |
. . 3
⊢ (¬
∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ (♯‘𝑥) = 1) ↔ ¬ ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
17 | | 19.3v 1991 |
. . . . . . . 8
⊢
(∀𝑎 𝑥 ∈ (Edg‘𝐺) ↔ 𝑥 ∈ (Edg‘𝐺)) |
18 | | 19.29 1881 |
. . . . . . . 8
⊢
((∀𝑎 𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎}) → ∃𝑎(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎})) |
19 | 17, 18 | sylanbr 585 |
. . . . . . 7
⊢ ((𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎}) → ∃𝑎(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎})) |
20 | | eleq1 2818 |
. . . . . . . . 9
⊢ (𝑥 = {𝑎} → (𝑥 ∈ (Edg‘𝐺) ↔ {𝑎} ∈ (Edg‘𝐺))) |
21 | 20 | biimpac 482 |
. . . . . . . 8
⊢ ((𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎}) → {𝑎} ∈ (Edg‘𝐺)) |
22 | 21 | eximi 1842 |
. . . . . . 7
⊢
(∃𝑎(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎}) → ∃𝑎{𝑎} ∈ (Edg‘𝐺)) |
23 | 19, 22 | syl 17 |
. . . . . 6
⊢ ((𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎}) → ∃𝑎{𝑎} ∈ (Edg‘𝐺)) |
24 | 23 | exlimiv 1938 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎}) → ∃𝑎{𝑎} ∈ (Edg‘𝐺)) |
25 | | dfclel 2810 |
. . . . . . . 8
⊢ ({𝑎} ∈ (Edg‘𝐺) ↔ ∃𝑥(𝑥 = {𝑎} ∧ 𝑥 ∈ (Edg‘𝐺))) |
26 | | pm3.22 463 |
. . . . . . . . 9
⊢ ((𝑥 = {𝑎} ∧ 𝑥 ∈ (Edg‘𝐺)) → (𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎})) |
27 | 26 | eximi 1842 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 = {𝑎} ∧ 𝑥 ∈ (Edg‘𝐺)) → ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎})) |
28 | 25, 27 | sylbi 220 |
. . . . . . 7
⊢ ({𝑎} ∈ (Edg‘𝐺) → ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎})) |
29 | 28 | eximi 1842 |
. . . . . 6
⊢
(∃𝑎{𝑎} ∈ (Edg‘𝐺) → ∃𝑎∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎})) |
30 | | excomim 2169 |
. . . . . 6
⊢
(∃𝑎∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎}) → ∃𝑥∃𝑎(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎})) |
31 | | 19.40 1894 |
. . . . . . . 8
⊢
(∃𝑎(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎}) → (∃𝑎 𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
32 | | ax5e 1920 |
. . . . . . . . 9
⊢
(∃𝑎 𝑥 ∈ (Edg‘𝐺) → 𝑥 ∈ (Edg‘𝐺)) |
33 | 32 | anim1i 618 |
. . . . . . . 8
⊢
((∃𝑎 𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎}) → (𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
34 | 31, 33 | syl 17 |
. . . . . . 7
⊢
(∃𝑎(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎}) → (𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
35 | 34 | eximi 1842 |
. . . . . 6
⊢
(∃𝑥∃𝑎(𝑥 ∈ (Edg‘𝐺) ∧ 𝑥 = {𝑎}) → ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
36 | 29, 30, 35 | 3syl 18 |
. . . . 5
⊢
(∃𝑎{𝑎} ∈ (Edg‘𝐺) → ∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎})) |
37 | 24, 36 | impbii 212 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎}) ↔ ∃𝑎{𝑎} ∈ (Edg‘𝐺)) |
38 | 37 | notbii 323 |
. . 3
⊢ (¬
∃𝑥(𝑥 ∈ (Edg‘𝐺) ∧ ∃𝑎 𝑥 = {𝑎}) ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺)) |
39 | 9, 16, 38 | 3bitri 300 |
. 2
⊢
(∀𝑥 ∈
(Edg‘𝐺)(♯‘𝑥) ≠ 1 ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺)) |
40 | 3, 39 | bitrdi 290 |
1
⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺))) |