Proof of Theorem umgr3v3e3cycl
Step | Hyp | Ref
| Expression |
1 | | umgrupgr 25769 |
. . . . . 6
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph
) |
2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) → 𝐺 ∈ UPGraph ) |
3 | | simpl 472 |
. . . . . 6
⊢ ((𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3) → 𝑓(CycleS‘𝐺)𝑝) |
4 | 3 | adantl 481 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) → 𝑓(CycleS‘𝐺)𝑝) |
5 | | simpr 476 |
. . . . . 6
⊢ ((𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3) → (#‘𝑓) = 3) |
6 | 5 | adantl 481 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) → (#‘𝑓) = 3) |
7 | | uhgr3cyclex.e |
. . . . . . 7
⊢ 𝐸 = (Edg‘𝐺) |
8 | | uhgr3cyclex.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
9 | 7, 8 | upgr3v3e3cycl 41347 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ 𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |
10 | | simpl 472 |
. . . . . . . . 9
⊢ ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) |
11 | 10 | reximi 2994 |
. . . . . . . 8
⊢
(∃𝑐 ∈
𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) → ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) |
12 | 11 | reximi 2994 |
. . . . . . 7
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) |
13 | 12 | reximi 2994 |
. . . . . 6
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) |
14 | 9, 13 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ 𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) |
15 | 2, 4, 6, 14 | syl3anc 1318 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) |
16 | 15 | ex 449 |
. . 3
⊢ (𝐺 ∈ UMGraph → ((𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸))) |
17 | 16 | exlimdvv 1849 |
. 2
⊢ (𝐺 ∈ UMGraph →
(∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸))) |
18 | | simplll 794 |
. . . . . 6
⊢ ((((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝐺 ∈ UMGraph ) |
19 | | df-3an 1033 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉)) |
20 | 19 | biimpri 217 |
. . . . . . 7
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
21 | 20 | ad4ant23 1289 |
. . . . . 6
⊢ ((((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
22 | | simpr 476 |
. . . . . 6
⊢ ((((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) |
23 | 8, 7 | umgr3cyclex 41350 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3 ∧ (𝑝‘0) = 𝑎)) |
24 | | 3simpa 1051 |
. . . . . . . 8
⊢ ((𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3 ∧ (𝑝‘0) = 𝑎) → (𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) |
25 | 24 | 2eximi 1753 |
. . . . . . 7
⊢
(∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3 ∧ (𝑝‘0) = 𝑎) → ∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) |
26 | 23, 25 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) |
27 | 18, 21, 22, 26 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3)) |
28 | 27 | ex 449 |
. . . 4
⊢ (((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3))) |
29 | 28 | rexlimdva 3013 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3))) |
30 | 29 | rexlimdvva 3020 |
. 2
⊢ (𝐺 ∈ UMGraph →
(∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3))) |
31 | 17, 30 | impbid 201 |
1
⊢ (𝐺 ∈ UMGraph →
(∃𝑓∃𝑝(𝑓(CycleS‘𝐺)𝑝 ∧ (#‘𝑓) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸))) |