Step |
Hyp |
Ref |
Expression |
1 |
|
dfsn2 |
⊢ { 𝐵 } = { 𝐵 , 𝐵 } |
2 |
1
|
opeq2i |
⊢ 〈 𝐴 , { 𝐵 } 〉 = 〈 𝐴 , { 𝐵 , 𝐵 } 〉 |
3 |
2
|
sneqi |
⊢ { 〈 𝐴 , { 𝐵 } 〉 } = { 〈 𝐴 , { 𝐵 , 𝐵 } 〉 } |
4 |
3
|
opeq2i |
⊢ 〈 𝑉 , { 〈 𝐴 , { 𝐵 } 〉 } 〉 = 〈 𝑉 , { 〈 𝐴 , { 𝐵 , 𝐵 } 〉 } 〉 |
5 |
|
3simpa |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ) |
6 |
|
id |
⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ 𝑉 ) |
7 |
6
|
ancri |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) |
8 |
7
|
3ad2ant3 |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) |
9 |
|
uspgr1eop |
⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 〈 𝑉 , { 〈 𝐴 , { 𝐵 , 𝐵 } 〉 } 〉 ∈ USPGraph ) |
10 |
5 8 9
|
syl2anc |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → 〈 𝑉 , { 〈 𝐴 , { 𝐵 , 𝐵 } 〉 } 〉 ∈ USPGraph ) |
11 |
4 10
|
eqeltrid |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → 〈 𝑉 , { 〈 𝐴 , { 𝐵 } 〉 } 〉 ∈ USPGraph ) |