Step |
Hyp |
Ref |
Expression |
1 |
|
uhgr3cyclex.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
uhgr3cyclex.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
umgrupgr |
⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph ) |
4 |
3
|
adantr |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → 𝐺 ∈ UPGraph ) |
5 |
|
simpl |
⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ) |
6 |
5
|
adantl |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ) |
7 |
|
simpr |
⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ( ♯ ‘ 𝑓 ) = 3 ) |
8 |
7
|
adantl |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → ( ♯ ‘ 𝑓 ) = 3 ) |
9 |
2 1
|
upgr3v3e3cycl |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) |
10 |
|
simpl |
⊢ ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) |
11 |
10
|
reximi |
⊢ ( ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) → ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) |
12 |
11
|
reximi |
⊢ ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) |
13 |
12
|
reximi |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) |
14 |
9 13
|
syl |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) |
15 |
4 6 8 14
|
syl3anc |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) |
16 |
15
|
ex |
⊢ ( 𝐺 ∈ UMGraph → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) |
17 |
16
|
exlimdvv |
⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) |
18 |
|
simplll |
⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → 𝐺 ∈ UMGraph ) |
19 |
|
df-3an |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) ) |
20 |
19
|
biimpri |
⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) |
21 |
20
|
ad4ant23 |
⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) |
22 |
|
simpr |
⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) |
23 |
1 2
|
umgr3cyclex |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) ) |
24 |
|
3simpa |
⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) |
25 |
24
|
2eximi |
⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) |
26 |
23 25
|
syl |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) |
27 |
18 21 22 26
|
syl3anc |
⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) |
28 |
27
|
rexlimdva2 |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) ) |
29 |
28
|
rexlimdvva |
⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) ) |
30 |
17 29
|
impbid |
⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) |