Step |
Hyp |
Ref |
Expression |
1 |
|
3cyclfrgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
3 |
1 2
|
3cyclfrgrrn |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) |
4 |
|
frgrusgr |
⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph ) |
5 |
|
usgrumgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph ) |
6 |
4 5
|
syl |
⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ UMGraph ) |
7 |
6
|
ad4antr |
⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝐺 ∈ UMGraph ) |
8 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 ) |
9 |
8
|
anim1i |
⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑣 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ) |
10 |
|
3anass |
⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ) |
11 |
9 10
|
sylibr |
⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) |
12 |
11
|
adantr |
⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) |
13 |
|
simpr |
⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) |
14 |
1 2
|
umgr3cyclex |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) |
15 |
7 12 13 14
|
syl3anc |
⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) |
16 |
15
|
ex |
⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) ) |
17 |
16
|
rexlimdvva |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) ) |
18 |
17
|
ralimdva |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ∀ 𝑣 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) ) |
19 |
3 18
|
mpd |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) |