Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 ) |
2 |
|
simpllr |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → 𝐴 ∈ 𝑋 ) |
3 |
|
simplrl |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → 𝐵 ∈ 𝑉 ) |
4 |
|
eleq2 |
⊢ ( ( Vtx ‘ 𝑔 ) = 𝑉 → ( 𝐵 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐵 ∈ 𝑉 ) ) |
5 |
4
|
ad2antrl |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → ( 𝐵 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐵 ∈ 𝑉 ) ) |
6 |
3 5
|
mpbird |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → 𝐵 ∈ ( Vtx ‘ 𝑔 ) ) |
7 |
|
simplrr |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → 𝐶 ∈ 𝑉 ) |
8 |
|
eleq2 |
⊢ ( ( Vtx ‘ 𝑔 ) = 𝑉 → ( 𝐶 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐶 ∈ 𝑉 ) ) |
9 |
8
|
ad2antrl |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → ( 𝐶 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐶 ∈ 𝑉 ) ) |
10 |
7 9
|
mpbird |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → 𝐶 ∈ ( Vtx ‘ 𝑔 ) ) |
11 |
|
simprr |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) |
12 |
1 2 6 10 11
|
upgr1e |
⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) ) → 𝑔 ∈ UPGraph ) |
13 |
12
|
ex |
⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) → 𝑔 ∈ UPGraph ) ) |
14 |
13
|
alrimiv |
⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) → 𝑔 ∈ UPGraph ) ) |
15 |
|
simpll |
⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑉 ∈ 𝑊 ) |
16 |
|
snex |
⊢ { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ∈ V |
17 |
16
|
a1i |
⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ∈ V ) |
18 |
14 15 17
|
gropeld |
⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 〈 𝑉 , { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } 〉 ∈ UPGraph ) |