Step |
Hyp |
Ref |
Expression |
1 |
|
prex |
⊢ { 𝐴 , 𝐵 } ∈ V |
2 |
|
s1val |
⊢ ( { 𝐴 , 𝐵 } ∈ V → 〈“ { 𝐴 , 𝐵 } ”〉 = { 〈 0 , { 𝐴 , 𝐵 } 〉 } ) |
3 |
1 2
|
mp1i |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 〈“ { 𝐴 , 𝐵 } ”〉 = { 〈 0 , { 𝐴 , 𝐵 } 〉 } ) |
4 |
3
|
opeq2d |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 〈 𝑉 , 〈“ { 𝐴 , 𝐵 } ”〉 〉 = 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 } 〉 ) |
5 |
|
simp1 |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑉 ∈ 𝑊 ) |
6 |
|
c0ex |
⊢ 0 ∈ V |
7 |
6
|
a1i |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 0 ∈ V ) |
8 |
|
3simpc |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) |
9 |
|
uspgr1eop |
⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 0 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 } 〉 ∈ USPGraph ) |
10 |
5 7 8 9
|
syl21anc |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 } 〉 ∈ USPGraph ) |
11 |
4 10
|
eqeltrd |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 〈 𝑉 , 〈“ { 𝐴 , 𝐵 } ”〉 〉 ∈ USPGraph ) |