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 ) |