| Step | Hyp | Ref
| Expression |
| 1 | | usgruspgr 29197 |
. . 3
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
USPGraph) |
| 2 | | edgusgr 29177 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝑒) = 2)) |
| 3 | 2 | simprd 495 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (♯‘𝑒) = 2) |
| 4 | 3 | ralrimiva 3146 |
. . 3
⊢ (𝐺 ∈ USGraph →
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) |
| 5 | 1, 4 | jca 511 |
. 2
⊢ (𝐺 ∈ USGraph → (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2)) |
| 6 | | edgval 29066 |
. . . . . . 7
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
| 8 | 7 | raleqdv 3326 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2 ↔ ∀𝑒 ∈ ran (iEdg‘𝐺)(♯‘𝑒) = 2)) |
| 9 | | eqid 2737 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 11 | 9, 10 | uspgrf 29171 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 12 | | f1f 6804 |
. . . . . . . . . 10
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 13 | 12 | frnd 6744 |
. . . . . . . . 9
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ ran (iEdg‘𝐺)
⊆ {𝑥 ∈
(𝒫 (Vtx‘𝐺)
∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) |
| 14 | | ssel2 3978 |
. . . . . . . . . . . . . . 15
⊢ ((ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (♯‘𝑥) ≤ 2} ∧ 𝑦 ∈ ran (iEdg‘𝐺)) → 𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 15 | 14 | expcom 413 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ 𝑦 ∈ {𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (♯‘𝑥) ≤ 2})) |
| 16 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑦 → ((♯‘𝑒) = 2 ↔ (♯‘𝑦) = 2)) |
| 17 | 16 | rspcv 3618 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (∀𝑒 ∈ ran (iEdg‘𝐺)(♯‘𝑒) = 2 →
(♯‘𝑦) =
2)) |
| 18 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
| 19 | 18 | breq1d 5153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) ≤ 2 ↔ (♯‘𝑦) ≤ 2)) |
| 20 | 19 | elrab 3692 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) ≤ 2)) |
| 21 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → 𝑦 ∈
𝒫 (Vtx‘𝐺)) |
| 22 | 21 | anim1i 615 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) = 2) → (𝑦 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝑦) = 2)) |
| 23 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) = 2 ↔ (♯‘𝑦) = 2)) |
| 24 | 23 | elrab 3692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2} ↔ (𝑦 ∈ 𝒫
(Vtx‘𝐺) ∧
(♯‘𝑦) =
2)) |
| 25 | 22, 24 | sylibr 234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) = 2) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
| 26 | 25 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → ((♯‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) ≤ 2) → ((♯‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 28 | 20, 27 | sylbi 217 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ ((♯‘𝑦) =
2 → 𝑦 ∈ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2})) |
| 29 | 17, 28 | syl9 77 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}))) |
| 30 | 15, 29 | syld 47 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}))) |
| 31 | 30 | com13 88 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}))) |
| 32 | 31 | imp 406 |
. . . . . . . . . . 11
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2})
→ (𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 33 | 32 | ssrdv 3989 |
. . . . . . . . . 10
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2})
→ ran (iEdg‘𝐺)
⊆ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2}) |
| 34 | 33 | ex 412 |
. . . . . . . . 9
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ ran (iEdg‘𝐺)
⊆ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2})) |
| 35 | 13, 34 | mpan9 506 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ ∀𝑒 ∈ ran
(iEdg‘𝐺)(♯‘𝑒) = 2) → ran (iEdg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
| 36 | | f1ssr 6810 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ ran (iEdg‘𝐺)
⊆ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) = 2})
→ (iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
| 37 | 35, 36 | syldan 591 |
. . . . . . 7
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ ∀𝑒 ∈ ran
(iEdg‘𝐺)(♯‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
| 38 | 37 | ex 412 |
. . . . . 6
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 39 | 11, 38 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(♯‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 40 | 8, 39 | sylbid 240 |
. . . 4
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 41 | 40 | imp 406 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
| 42 | 9, 10 | isusgrs 29173 |
. . . 4
⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 43 | 42 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) → (𝐺 ∈ USGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
| 44 | 41, 43 | mpbird 257 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) → 𝐺 ∈ USGraph) |
| 45 | 5, 44 | impbii 209 |
1
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2)) |