Step |
Hyp |
Ref |
Expression |
1 |
|
umgrnloopv.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
2 |
|
umgredgprv.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
3 |
|
umgruhgr |
⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph ) |
4 |
2 1
|
uhgrss |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ) |
5 |
3 4
|
sylan |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ) |
6 |
2 1
|
umgredg2 |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) |
7 |
|
sseq1 |
⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) ) |
8 |
|
fveqeq2 |
⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) ) |
9 |
7 8
|
anbi12d |
⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) ↔ ( { 𝑀 , 𝑁 } ⊆ 𝑉 ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) ) ) |
10 |
|
eqid |
⊢ { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 } |
11 |
10
|
hashprdifel |
⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) ) |
12 |
|
prssg |
⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) ) |
13 |
12
|
3adant3 |
⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) ) |
14 |
13
|
biimprd |
⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) → ( { 𝑀 , 𝑁 } ⊆ 𝑉 → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) |
15 |
11 14
|
syl |
⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( { 𝑀 , 𝑁 } ⊆ 𝑉 → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) |
16 |
15
|
impcom |
⊢ ( ( { 𝑀 , 𝑁 } ⊆ 𝑉 ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) |
17 |
9 16
|
syl6bi |
⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) |
18 |
17
|
com12 |
⊢ ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) |
19 |
5 6 18
|
syl2anc |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) |