Step |
Hyp |
Ref |
Expression |
1 |
|
usgrop |
⊢ ( 𝐺 ∈ USGraph → 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ USGraph ) |
2 |
|
cplgrop |
⊢ ( 𝐺 ∈ ComplGraph → 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ ComplGraph ) |
3 |
1 2
|
anim12i |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) → ( 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ USGraph ∧ 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ ComplGraph ) ) |
4 |
|
iscusgr |
⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) ) |
5 |
|
iscusgr |
⊢ ( 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ ComplUSGraph ↔ ( 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ USGraph ∧ 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ ComplGraph ) ) |
6 |
3 4 5
|
3imtr4i |
⊢ ( 𝐺 ∈ ComplUSGraph → 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ ComplUSGraph ) |