| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elopab 5532 | . . . . 5
⊢ (𝑝 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ↔ ∃𝑣∃𝑒(𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅)) | 
| 2 |  | f0bi 6791 | . . . . . . . . . 10
⊢ (𝑒:∅⟶∅ ↔
𝑒 =
∅) | 
| 3 |  | opeq2 4874 | . . . . . . . . . . . 12
⊢ (𝑒 = ∅ → 〈𝑣, 𝑒〉 = 〈𝑣, ∅〉) | 
| 4 |  | usgr0eop 29263 | . . . . . . . . . . . . 13
⊢ (𝑣 ∈ V → 〈𝑣, ∅〉 ∈
USGraph) | 
| 5 | 4 | elv 3485 | . . . . . . . . . . . 12
⊢
〈𝑣,
∅〉 ∈ USGraph | 
| 6 | 3, 5 | eqeltrdi 2849 | . . . . . . . . . . 11
⊢ (𝑒 = ∅ → 〈𝑣, 𝑒〉 ∈ USGraph) | 
| 7 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑣 ∈ V | 
| 8 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑒 ∈ V | 
| 9 | 7, 8 | opiedgfvi 29027 | . . . . . . . . . . . 12
⊢
(iEdg‘〈𝑣,
𝑒〉) = 𝑒 | 
| 10 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑒 = ∅ → 𝑒 = ∅) | 
| 11 | 9, 10 | eqtrid 2789 | . . . . . . . . . . 11
⊢ (𝑒 = ∅ →
(iEdg‘〈𝑣, 𝑒〉) =
∅) | 
| 12 | 6, 11 | jca 511 | . . . . . . . . . 10
⊢ (𝑒 = ∅ → (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) | 
| 13 | 2, 12 | sylbi 217 | . . . . . . . . 9
⊢ (𝑒:∅⟶∅ →
(〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) | 
| 14 | 13 | adantl 481 | . . . . . . . 8
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅)) | 
| 15 |  | eleq1 2829 | . . . . . . . . . 10
⊢ (𝑝 = 〈𝑣, 𝑒〉 → (𝑝 ∈ USGraph ↔ 〈𝑣, 𝑒〉 ∈ USGraph)) | 
| 16 |  | fveqeq2 6915 | . . . . . . . . . 10
⊢ (𝑝 = 〈𝑣, 𝑒〉 → ((iEdg‘𝑝) = ∅ ↔ (iEdg‘〈𝑣, 𝑒〉) = ∅)) | 
| 17 | 15, 16 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑝 = 〈𝑣, 𝑒〉 → ((𝑝 ∈ USGraph ∧ (iEdg‘𝑝) = ∅) ↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅))) | 
| 18 | 17 | adantr 480 | . . . . . . . 8
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → ((𝑝 ∈ USGraph ∧
(iEdg‘𝑝) = ∅)
↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(iEdg‘〈𝑣, 𝑒〉) =
∅))) | 
| 19 | 14, 18 | mpbird 257 | . . . . . . 7
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → (𝑝 ∈ USGraph ∧
(iEdg‘𝑝) =
∅)) | 
| 20 |  | fveqeq2 6915 | . . . . . . . 8
⊢ (𝑔 = 𝑝 → ((iEdg‘𝑔) = ∅ ↔ (iEdg‘𝑝) = ∅)) | 
| 21 | 20 | elrab 3692 | . . . . . . 7
⊢ (𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} ↔ (𝑝 ∈ USGraph ∧
(iEdg‘𝑝) =
∅)) | 
| 22 | 19, 21 | sylibr 234 | . . . . . 6
⊢ ((𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) | 
| 23 | 22 | exlimivv 1932 | . . . . 5
⊢
(∃𝑣∃𝑒(𝑝 = 〈𝑣, 𝑒〉 ∧ 𝑒:∅⟶∅) → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) | 
| 24 | 1, 23 | sylbi 217 | . . . 4
⊢ (𝑝 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} → 𝑝 ∈ {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅}) | 
| 25 | 24 | ssriv 3987 | . . 3
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⊆
{𝑔 ∈ USGraph ∣
(iEdg‘𝑔) =
∅} | 
| 26 |  | eqid 2737 | . . . 4
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} =
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} | 
| 27 | 26 | griedg0prc 29281 | . . 3
⊢
{〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ∉
V | 
| 28 |  | prcssprc 5327 | . . 3
⊢
(({〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⊆
{𝑔 ∈ USGraph ∣
(iEdg‘𝑔) = ∅}
∧ {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ∉
V) → {𝑔 ∈ USGraph
∣ (iEdg‘𝑔) =
∅} ∉ V) | 
| 29 | 25, 27, 28 | mp2an 692 | . 2
⊢ {𝑔 ∈ USGraph ∣
(iEdg‘𝑔) = ∅}
∉ V | 
| 30 |  | df-3an 1089 | . . . . . . . 8
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0) ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0)) | 
| 31 | 30 | bicomi 224 | . . . . . . 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 12605 | . . . . . . 7
⊢ 0 ∈
ℕ0* | 
| 34 |  | ibar 528 | . . . . . . 7
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) → (∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) | 
| 35 | 33, 34 | mpan2 691 | . . . . . 6
⊢ (𝑔 ∈ USGraph →
(∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0 ↔ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) | 
| 36 |  | eqid 2737 | . . . . . . . 8
⊢
(Vtx‘𝑔) =
(Vtx‘𝑔) | 
| 37 |  | eqid 2737 | . . . . . . . 8
⊢
(VtxDeg‘𝑔) =
(VtxDeg‘𝑔) | 
| 38 | 36, 37 | isrusgr0 29584 | . . . . . . 7
⊢ ((𝑔 ∈ USGraph ∧ 0 ∈
ℕ0*) → (𝑔 RegUSGraph 0 ↔ (𝑔 ∈ USGraph ∧ 0 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0))) | 
| 39 | 33, 38 | mpan2 691 | . . . . . 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 3440 | . . . 4
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0} | 
| 42 |  | usgr0edg0rusgr 29593 | . . . . . 6
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔
(Edg‘𝑔) =
∅)) | 
| 43 |  | usgruhgr 29203 | . . . . . . 7
⊢ (𝑔 ∈ USGraph → 𝑔 ∈
UHGraph) | 
| 44 |  | uhgriedg0edg0 29144 | . . . . . . 7
⊢ (𝑔 ∈ UHGraph →
((Edg‘𝑔) = ∅
↔ (iEdg‘𝑔) =
∅)) | 
| 45 | 43, 44 | syl 17 | . . . . . 6
⊢ (𝑔 ∈ USGraph →
((Edg‘𝑔) = ∅
↔ (iEdg‘𝑔) =
∅)) | 
| 46 | 42, 45 | bitrd 279 | . . . . 5
⊢ (𝑔 ∈ USGraph → (𝑔 RegUSGraph 0 ↔
(iEdg‘𝑔) =
∅)) | 
| 47 | 46 | rabbiia 3440 | . . . 4
⊢ {𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0} = {𝑔 ∈ USGraph ∣
(iEdg‘𝑔) =
∅} | 
| 48 | 41, 47 | eqtri 2765 | . . 3
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} = {𝑔 ∈ USGraph ∣ (iEdg‘𝑔) = ∅} | 
| 49 |  | neleq1 3052 | . . 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 231 | 1
⊢ {𝑔 ∈ USGraph ∣
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V |