Step |
Hyp |
Ref |
Expression |
1 |
|
fveqeq2 |
⊢ ( 𝑦 = 𝑥 → ( ( ♯ ‘ 𝑦 ) = 2 ↔ ( ♯ ‘ 𝑥 ) = 2 ) ) |
2 |
1
|
cbvrabv |
⊢ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } |
3 |
2
|
cusgrexilem1 |
⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) ∈ V ) |
4 |
2
|
cusgrexi |
⊢ ( 𝑉 ∈ 𝑊 → 〈 𝑉 , ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) 〉 ∈ ComplUSGraph ) |
5 |
|
opeq2 |
⊢ ( 𝑒 = ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) → 〈 𝑉 , 𝑒 〉 = 〈 𝑉 , ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) 〉 ) |
6 |
5
|
eleq1d |
⊢ ( 𝑒 = ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) → ( 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ↔ 〈 𝑉 , ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) 〉 ∈ ComplUSGraph ) ) |
7 |
3 4 6
|
spcedv |
⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑒 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ) |