Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
3 |
1 2
|
isumgr |
⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ UMGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
4 |
|
id |
⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
5 |
|
2re |
⊢ 2 ∈ ℝ |
6 |
5
|
leidi |
⊢ 2 ≤ 2 |
7 |
6
|
a1i |
⊢ ( ( ♯ ‘ 𝑥 ) = 2 → 2 ≤ 2 ) |
8 |
|
breq1 |
⊢ ( ( ♯ ‘ 𝑥 ) = 2 → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ 2 ≤ 2 ) ) |
9 |
7 8
|
mpbird |
⊢ ( ( ♯ ‘ 𝑥 ) = 2 → ( ♯ ‘ 𝑥 ) ≤ 2 ) |
10 |
9
|
a1i |
⊢ ( 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( ( ♯ ‘ 𝑥 ) = 2 → ( ♯ ‘ 𝑥 ) ≤ 2 ) ) |
11 |
10
|
ss2rabi |
⊢ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } |
12 |
11
|
a1i |
⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
13 |
4 12
|
fssd |
⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
14 |
3 13
|
syl6bi |
⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ UMGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
15 |
14
|
pm2.43i |
⊢ ( 𝐺 ∈ UMGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
16 |
1 2
|
isupgr |
⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
17 |
15 16
|
mpbird |
⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph ) |