Step | Hyp | Ref
| Expression |
1 | | frisusgra 26519 |
. . . 4
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | 4cycl4dv4e 26196 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) |
3 | | frisusgrapr 26518 |
. . . . . . . . . . . . 13
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
4 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → 𝑐 ∈ 𝑉) |
5 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝑐 ∈ 𝑉) |
6 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → 𝑐 ∈ 𝑉) |
7 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ≠ 𝑐 ↔ 𝑐 ≠ 𝑎) |
8 | 7 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ≠ 𝑐 → 𝑐 ≠ 𝑎) |
9 | 8 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) → 𝑐 ≠ 𝑎) |
10 | 9 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) → 𝑐 ≠ 𝑎) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → 𝑐 ≠ 𝑎) |
12 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑐 ∈ 𝑉 ∧ 𝑐 ≠ 𝑎)) |
13 | 6, 11, 12 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → 𝑐 ∈ (𝑉 ∖ {𝑎})) |
14 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑎 → {𝑘} = {𝑎}) |
15 | 14 | difeq2d 3690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑎 → (𝑉 ∖ {𝑘}) = (𝑉 ∖ {𝑎})) |
16 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑎 → {𝑥, 𝑘} = {𝑥, 𝑎}) |
17 | 16 | preq1d 4218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑎 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝑎}, {𝑥, 𝑙}}) |
18 | 17 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑎 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
19 | 18 | reubidv 3103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑎 → (∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
20 | 15, 19 | raleqbidv 3129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑎 → (∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ (𝑉 ∖ {𝑎})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
21 | 20 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ∀𝑙 ∈ (𝑉 ∖ {𝑎})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ∀𝑙 ∈ (𝑉 ∖ {𝑎})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ∀𝑙 ∈ (𝑉 ∖ {𝑎})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ∀𝑙 ∈ (𝑉 ∖ {𝑎})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
25 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑐 → {𝑥, 𝑙} = {𝑥, 𝑐}) |
26 | 25 | preq2d 4219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑐 → {{𝑥, 𝑎}, {𝑥, 𝑙}} = {{𝑥, 𝑎}, {𝑥, 𝑐}}) |
27 | 26 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑐 → ({{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝑎}, {𝑥, 𝑐}} ⊆ ran 𝐸)) |
28 | 27 | reubidv 3103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑐 → (∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑐}} ⊆ ran 𝐸)) |
29 | 28 | rspcv 3278 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ (𝑉 ∖ {𝑎}) → (∀𝑙 ∈ (𝑉 ∖ {𝑎})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑐}} ⊆ ran 𝐸)) |
30 | 13, 24, 29 | sylsyld 59 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑎}, {𝑥, 𝑐}} ⊆ ran 𝐸)) |
31 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑥, 𝑎} = {𝑎, 𝑥} |
32 | 31 | preq1i 4215 |
. . . . . . . . . . . . . . . . . . 19
⊢ {{𝑥, 𝑎}, {𝑥, 𝑐}} = {{𝑎, 𝑥}, {𝑥, 𝑐}} |
33 | 32 | sseq1i 3592 |
. . . . . . . . . . . . . . . . . 18
⊢ ({{𝑥, 𝑎}, {𝑥, 𝑐}} ⊆ ran 𝐸 ↔ {{𝑎, 𝑥}, {𝑥, 𝑐}} ⊆ ran 𝐸) |
34 | 33 | reubii 3105 |
. . . . . . . . . . . . . . . . 17
⊢
(∃!𝑥 ∈
𝑉 {{𝑥, 𝑎}, {𝑥, 𝑐}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ 𝑉 {{𝑎, 𝑥}, {𝑥, 𝑐}} ⊆ ran 𝐸) |
35 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) → ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |
36 | 35 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |
37 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) → ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) |
38 | 37 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) |
39 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝑏 ∈ 𝑉) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → 𝑏 ∈ 𝑉) |
42 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → 𝑑 ∈ 𝑉) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝑑 ∈ 𝑉) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → 𝑑 ∈ 𝑉) |
45 | | simprr2 1103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) → 𝑏 ≠ 𝑑) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → 𝑏 ≠ 𝑑) |
47 | | 4cycl2vnunb 26544 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸) ∧ (𝑏 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ∧ 𝑏 ≠ 𝑑)) → ¬ ∃!𝑥 ∈ 𝑉 {{𝑎, 𝑥}, {𝑥, 𝑐}} ⊆ ran 𝐸) |
48 | 36, 38, 41, 44, 46, 47 | syl113anc 1330 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → ¬ ∃!𝑥 ∈ 𝑉 {{𝑎, 𝑥}, {𝑥, 𝑐}} ⊆ ran 𝐸) |
49 | 48 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (∃!𝑥 ∈ 𝑉 {{𝑎, 𝑥}, {𝑥, 𝑐}} ⊆ ran 𝐸 → (#‘𝐹) ≠ 4)) |
50 | 49 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
(∃!𝑥 ∈
𝑉 {{𝑎, 𝑥}, {𝑥, 𝑐}} ⊆ ran 𝐸 → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (#‘𝐹) ≠ 4)) |
51 | 34, 50 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢
(∃!𝑥 ∈
𝑉 {{𝑥, 𝑎}, {𝑥, 𝑐}} ⊆ ran 𝐸 → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (#‘𝐹) ≠ 4)) |
52 | 30, 51 | syl6 34 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (#‘𝐹) ≠ 4))) |
53 | 52 | pm2.43b 53 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (#‘𝐹) ≠ 4)) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸) → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (#‘𝐹) ≠ 4)) |
55 | 3, 54 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑉 FriendGrph 𝐸 → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (#‘𝐹) ≠ 4)) |
56 | 55 | com12 32 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) ∧ ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → (𝑉 FriendGrph 𝐸 → (#‘𝐹) ≠ 4)) |
57 | 56 | ex 449 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) → (𝑉 FriendGrph 𝐸 → (#‘𝐹) ≠ 4))) |
58 | 57 | rexlimdvva 3020 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) → (𝑉 FriendGrph 𝐸 → (#‘𝐹) ≠ 4))) |
59 | 58 | rexlimivv 3018 |
. . . . . . . 8
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) → (𝑉 FriendGrph 𝐸 → (#‘𝐹) ≠ 4)) |
60 | 2, 59 | syl 17 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 4) → (𝑉 FriendGrph 𝐸 → (#‘𝐹) ≠ 4)) |
61 | 60 | 3exp 1256 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝐹(𝑉 Cycles 𝐸)𝑃 → ((#‘𝐹) = 4 → (𝑉 FriendGrph 𝐸 → (#‘𝐹) ≠ 4)))) |
62 | 61 | com34 89 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 FriendGrph 𝐸 → ((#‘𝐹) = 4 → (#‘𝐹) ≠ 4)))) |
63 | 62 | com23 84 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 FriendGrph 𝐸 → (𝐹(𝑉 Cycles 𝐸)𝑃 → ((#‘𝐹) = 4 → (#‘𝐹) ≠ 4)))) |
64 | 1, 63 | mpcom 37 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → (𝐹(𝑉 Cycles 𝐸)𝑃 → ((#‘𝐹) = 4 → (#‘𝐹) ≠ 4))) |
65 | 64 | imp 444 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃) → ((#‘𝐹) = 4 → (#‘𝐹) ≠ 4)) |
66 | | df-ne 2782 |
. . 3
⊢
((#‘𝐹) ≠ 4
↔ ¬ (#‘𝐹) =
4) |
67 | 66 | biimpri 217 |
. 2
⊢ (¬
(#‘𝐹) = 4 →
(#‘𝐹) ≠
4) |
68 | 65, 67 | pm2.61d1 170 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 4) |