| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 2 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
| 3 |
1 2
|
upgrf |
⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) |
| 4 |
|
fvex |
⊢ ( Vtx ‘ 𝐺 ) ∈ V |
| 5 |
|
fvex |
⊢ ( iEdg ‘ 𝐺 ) ∈ V |
| 6 |
4 5
|
pm3.2i |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) |
| 7 |
|
opex |
⊢ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ V |
| 8 |
|
eqid |
⊢ ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) |
| 9 |
|
eqid |
⊢ ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) |
| 10 |
8 9
|
isupgr |
⊢ ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ V → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) : dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) |
| 11 |
7 10
|
mp1i |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) : dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) |
| 12 |
|
opiedgfv |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( iEdg ‘ 𝐺 ) ) |
| 13 |
12
|
dmeqd |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = dom ( iEdg ‘ 𝐺 ) ) |
| 14 |
|
opvtxfv |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( Vtx ‘ 𝐺 ) ) |
| 15 |
14
|
pweqd |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = 𝒫 ( Vtx ‘ 𝐺 ) ) |
| 16 |
15
|
difeq1d |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) |
| 17 |
16
|
rabeqdv |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } = { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) |
| 18 |
12 13 17
|
feq123d |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) : dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) |
| 19 |
11 18
|
bitrd |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) |
| 20 |
6 19
|
mp1i |
⊢ ( 𝐺 ∈ UPGraph → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) |
| 21 |
3 20
|
mpbird |
⊢ ( 𝐺 ∈ UPGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ) |