Step | Hyp | Ref
| Expression |
1 | | elopab 5442 |
. . . . 5
⊢ (𝑝 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ↔ ∃𝑣∃𝑒(𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅)) |
2 | | f0bi 6659 |
. . . . . . . . . 10
⊢ (𝑒:∅⟶∅ ↔
𝑒 =
∅) |
3 | | opeq2 4807 |
. . . . . . . . . . . 12
⊢ (𝑒 = ∅ → 〈𝑣, 𝑒〉 = 〈𝑣, ∅〉) |
4 | | usgr0eop 27611 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ V → 〈𝑣, ∅〉 ∈
USGraph) |
5 | 4 | elv 3437 |
. . . . . . . . . . . 12
⊢
〈𝑣,
∅〉 ∈ USGraph |
6 | 3, 5 | eqeltrdi 2847 |
. . . . . . . . . . 11
⊢ (𝑒 = ∅ → 〈𝑣, 𝑒〉 ∈ USGraph) |
7 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑣 ∈ V |
8 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑒 ∈ V |
9 | 7, 8 | opiedgfvi 27378 |
. . . . . . . . . . . 12
⊢
(iEdg‘〈𝑣,
𝑒〉) = 𝑒 |
10 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑒 = ∅ → 𝑒 = ∅) |
11 | 9, 10 | eqtrid 2790 |
. . . . . . . . . . 11
⊢ (𝑒 = ∅ →
(iEdg‘〈𝑣, 𝑒〉) =
∅) |
12 | 6, 11 | jca 512 |
. . . . . . . . . 10
⊢ (𝑒 = ∅ → (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) |
13 | 2, 12 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑒:∅⟶∅ →
(〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) |
14 | 13 | adantl 482 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) |
15 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑣, 𝑒〉 → (𝑝 ∈ USGraph ↔ 〈𝑣, 𝑒〉 ∈ USGraph)) |
16 | | fveqeq2 6785 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑣, 𝑒〉 → ((iEdg‘𝑝) = ∅ ↔ (iEdg‘〈𝑣, 𝑒〉) = ∅)) |
17 | 15, 16 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑣, 𝑒〉 → ((𝑝 ∈ USGraph ∧ (iEdg‘𝑝) = ∅) ↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅))) |
18 | 17 | adantr 481 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → ((𝑝 ∈ USGraph ∧
(iEdg‘𝑝) = ∅)
↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅))) |
19 | 14, 18 | mpbird 256 |
. . . . . . 7
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → (𝑝 ∈ USGraph ∧
(iEdg‘𝑝) =
∅)) |
20 | | fveqeq2 6785 |
. . . . . . . 8
⊢ (𝑔 = 𝑝 → ((iEdg‘𝑔) = ∅ ↔ (iEdg‘𝑝) = ∅)) |
21 | 20 | elrab 3625 |
. . . . . . 7
⊢ (𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} ↔ (𝑝 ∈ USGraph ∧
(iEdg‘𝑝) =
∅)) |
22 | 19, 21 | sylibr 233 |
. . . . . 6
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) |
23 | 22 | exlimivv 1935 |
. . . . 5
⊢
(∃𝑣∃𝑒(𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) |
24 | 1, 23 | sylbi 216 |
. . . 4
⊢ (𝑝 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) |
25 | 24 | ssriv 3926 |
. . 3
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⊆
{𝑔 ∈ USGraph ∣
(iEdg‘𝑔) =
∅} |
26 | | eqid 2738 |
. . . 4
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} =
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} |
27 | 26 | griedg0prc 27629 |
. . 3
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ∉
V |
28 | | prcssprc 5251 |
. . 3
⊢
(({〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⊆
{𝑔 ∈ USGraph ∣
(iEdg‘𝑔) = ∅}
∧ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ∉
V) → {𝑔 ∈ USGraph
∣ (iEdg‘𝑔) =
∅} ∉ V) |
29 | 25, 27, 28 | mp2an 689 |
. 2
⊢ {𝑔 ∈ USGraph ∣
(iEdg‘𝑔) = ∅}
∉ V |
30 | | df-3an 1088 |
. . . . . . . 8
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0) ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0)) |
31 | 30 | bicomi 223 |
. . . . . . 7
⊢ (((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0) ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0)) |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝑔 ∈ USGraph → (((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0) ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
33 | | 0xnn0 12309 |
. . . . . . 7
⊢ 0 ∈
ℕ0* |
34 | | ibar 529 |
. . . . . . 7
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) → (∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
35 | 33, 34 | mpan2 688 |
. . . . . 6
⊢ (𝑔 ∈ USGraph →
(∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
36 | | eqid 2738 |
. . . . . . . 8
⊢
(Vtx‘𝑔) =
(Vtx‘𝑔) |
37 | | eqid 2738 |
. . . . . . . 8
⊢
(VtxDeg‘𝑔) =
(VtxDeg‘𝑔) |
38 | 36, 37 | isrusgr0 27931 |
. . . . . . 7
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) → (𝑔 RegUSGraph 0 ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
39 | 33, 38 | mpan2 688 |
. . . . . 6
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
40 | 32, 35, 39 | 3bitr4d 311 |
. . . . 5
⊢ (𝑔 ∈ USGraph →
(∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ 𝑔 RegUSGraph 0)) |
41 | 40 | rabbiia 3406 |
. . . 4
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0} |
42 | | usgr0edg0rusgr 27940 |
. . . . . 6
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔
(Edg‘𝑔) =
∅)) |
43 | | usgruhgr 27551 |
. . . . . . 7
⊢ (𝑔 ∈ USGraph → 𝑔 ∈
UHGraph) |
44 | | uhgriedg0edg0 27495 |
. . . . . . 7
⊢ (𝑔 ∈ UHGraph →
((Edg‘𝑔) = ∅
↔ (iEdg‘𝑔) =
∅)) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝑔 ∈ USGraph →
((Edg‘𝑔) = ∅
↔ (iEdg‘𝑔) =
∅)) |
46 | 42, 45 | bitrd 278 |
. . . . 5
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔
(iEdg‘𝑔) =
∅)) |
47 | 46 | rabbiia 3406 |
. . . 4
⊢ {𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0} = {𝑔 ∈ USGraph ∣
(iEdg‘𝑔) =
∅} |
48 | 41, 47 | eqtri 2766 |
. . 3
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} |
49 | | neleq1 3054 |
. . 3
⊢ ({𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} → ({𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V ↔ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} ∉
V)) |
50 | 48, 49 | ax-mp 5 |
. 2
⊢ ({𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V ↔ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} ∉
V) |
51 | 29, 50 | mpbir 230 |
1
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V |