Step | Hyp | Ref
| Expression |
1 | | elopab 4908 |
. . . . 5
⊢ (𝑝 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ↔ ∃𝑣∃𝑒(𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅)) |
2 | | f0bi 6001 |
. . . . . . . . . 10
⊢ (𝑒:∅⟶∅ ↔
𝑒 =
∅) |
3 | | opeq2 4341 |
. . . . . . . . . . . 12
⊢ (𝑒 = ∅ → 〈𝑣, 𝑒〉 = 〈𝑣, ∅〉) |
4 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑣 ∈ V |
5 | | usgr0eop 40472 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ V → 〈𝑣, ∅〉 ∈ USGraph
) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
〈𝑣,
∅〉 ∈ USGraph |
7 | 3, 6 | syl6eqel 2696 |
. . . . . . . . . . 11
⊢ (𝑒 = ∅ → 〈𝑣, 𝑒〉 ∈ USGraph ) |
8 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑒 ∈ V |
9 | | opiedgfv 25684 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) →
(iEdg‘〈𝑣, 𝑒〉) = 𝑒) |
10 | 4, 8, 9 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(iEdg‘〈𝑣,
𝑒〉) = 𝑒 |
11 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑒 = ∅ → 𝑒 = ∅) |
12 | 10, 11 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (𝑒 = ∅ →
(iEdg‘〈𝑣, 𝑒〉) =
∅) |
13 | 7, 12 | jca 553 |
. . . . . . . . . 10
⊢ (𝑒 = ∅ → (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) |
14 | 2, 13 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑒:∅⟶∅ →
(〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) |
15 | 14 | adantl 481 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) |
16 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑣, 𝑒〉 → (𝑝 ∈ USGraph ↔ 〈𝑣, 𝑒〉 ∈ USGraph )) |
17 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑣, 𝑒〉 → (iEdg‘𝑝) = (iEdg‘〈𝑣, 𝑒〉)) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑣, 𝑒〉 → ((iEdg‘𝑝) = ∅ ↔ (iEdg‘〈𝑣, 𝑒〉) = ∅)) |
19 | 16, 18 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑣, 𝑒〉 → ((𝑝 ∈ USGraph ∧ (iEdg‘𝑝) = ∅) ↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅))) |
20 | 19 | adantr 480 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → ((𝑝 ∈ USGraph ∧
(iEdg‘𝑝) = ∅)
↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅))) |
21 | 15, 20 | mpbird 246 |
. . . . . . 7
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → (𝑝 ∈ USGraph ∧
(iEdg‘𝑝) =
∅)) |
22 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = 𝑝 → (iEdg‘𝑔) = (iEdg‘𝑝)) |
23 | 22 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑔 = 𝑝 → ((iEdg‘𝑔) = ∅ ↔ (iEdg‘𝑝) = ∅)) |
24 | 23 | elrab 3331 |
. . . . . . 7
⊢ (𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} ↔ (𝑝 ∈ USGraph ∧
(iEdg‘𝑝) =
∅)) |
25 | 21, 24 | sylibr 223 |
. . . . . 6
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) |
26 | 25 | exlimivv 1847 |
. . . . 5
⊢
(∃𝑣∃𝑒(𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) |
27 | 1, 26 | sylbi 206 |
. . . 4
⊢ (𝑝 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) |
28 | 27 | ssriv 3572 |
. . 3
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⊆
{𝑔 ∈ USGraph ∣
(iEdg‘𝑔) =
∅} |
29 | | eqid 2610 |
. . . 4
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} =
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} |
30 | 29 | griedg0prc 40488 |
. . 3
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ∉
V |
31 | | prcssprc 40306 |
. . 3
⊢
(({〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⊆
{𝑔 ∈ USGraph ∣
(iEdg‘𝑔) = ∅}
∧ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ∉
V) → {𝑔 ∈ USGraph
∣ (iEdg‘𝑔) =
∅} ∉ V) |
32 | 28, 30, 31 | mp2an 704 |
. 2
⊢ {𝑔 ∈ USGraph ∣
(iEdg‘𝑔) = ∅}
∉ V |
33 | | df-3an 1033 |
. . . . . . . 8
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0) ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0)) |
34 | 33 | bicomi 213 |
. . . . . . 7
⊢ (((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0) ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0)) |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝑔 ∈ USGraph → (((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0) ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
36 | | 0xnn0 11246 |
. . . . . . 7
⊢ 0 ∈
ℕ0* |
37 | | ibar 524 |
. . . . . . 7
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) → (∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
38 | 36, 37 | mpan2 703 |
. . . . . 6
⊢ (𝑔 ∈ USGraph →
(∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
39 | | eqid 2610 |
. . . . . . . 8
⊢
(Vtx‘𝑔) =
(Vtx‘𝑔) |
40 | | eqid 2610 |
. . . . . . . 8
⊢
(VtxDeg‘𝑔) =
(VtxDeg‘𝑔) |
41 | 39, 40 | isrusgr0 40766 |
. . . . . . 7
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) → (𝑔 RegUSGraph 0 ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
42 | 36, 41 | mpan2 703 |
. . . . . 6
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) |
43 | 35, 38, 42 | 3bitr4d 299 |
. . . . 5
⊢ (𝑔 ∈ USGraph →
(∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ 𝑔 RegUSGraph 0)) |
44 | 43 | rabbiia 3161 |
. . . 4
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0} |
45 | | usgr0edg0rusgr 40775 |
. . . . . 6
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔
(Edg‘𝑔) =
∅)) |
46 | | usgruhgr 40413 |
. . . . . . 7
⊢ (𝑔 ∈ USGraph → 𝑔 ∈ UHGraph
) |
47 | | uhgriedg0edg0 25801 |
. . . . . . 7
⊢ (𝑔 ∈ UHGraph →
((Edg‘𝑔) = ∅
↔ (iEdg‘𝑔) =
∅)) |
48 | 46, 47 | syl 17 |
. . . . . 6
⊢ (𝑔 ∈ USGraph →
((Edg‘𝑔) = ∅
↔ (iEdg‘𝑔) =
∅)) |
49 | 45, 48 | bitrd 267 |
. . . . 5
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔
(iEdg‘𝑔) =
∅)) |
50 | 49 | rabbiia 3161 |
. . . 4
⊢ {𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0} = {𝑔 ∈ USGraph ∣
(iEdg‘𝑔) =
∅} |
51 | 44, 50 | eqtri 2632 |
. . 3
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} |
52 | | neleq1 2888 |
. . 3
⊢ ({𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} → ({𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V ↔ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} ∉
V)) |
53 | 51, 52 | ax-mp 5 |
. 2
⊢ ({𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V ↔ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} ∉
V) |
54 | 32, 53 | mpbir 220 |
1
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V |