Step | Hyp | Ref
| Expression |
1 | | simprl 790 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
2 | | simprr 792 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))) → ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) |
3 | | simpl3 1059 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))) → (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) |
4 | | 4cycl2vnunb 26544 |
. . . . 5
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸) |
5 | 1, 2, 3, 4 | syl3anc 1318 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))) → ¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸) |
6 | | frgraunss 26522 |
. . . . . . . 8
⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸)) |
7 | | pm2.24 120 |
. . . . . . . 8
⊢
(∃!𝑥 ∈
𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸 → (¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸 → ¬ 𝑉 FriendGrph 𝐸)) |
8 | 6, 7 | syl6com 36 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → (𝑉 FriendGrph 𝐸 → (¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸 → ¬ 𝑉 FriendGrph 𝐸))) |
9 | 8 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → (𝑉 FriendGrph 𝐸 → (¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸 → ¬ 𝑉 FriendGrph 𝐸))) |
10 | 9 | com23 84 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → (¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸 → (𝑉 FriendGrph 𝐸 → ¬ 𝑉 FriendGrph 𝐸))) |
11 | 10 | adantr 480 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))) → (¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸 → (𝑉 FriendGrph 𝐸 → ¬ 𝑉 FriendGrph 𝐸))) |
12 | 5, 11 | mpd 15 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))) → (𝑉 FriendGrph 𝐸 → ¬ 𝑉 FriendGrph 𝐸)) |
13 | 12 | pm2.01d 180 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))) → ¬ 𝑉 FriendGrph 𝐸) |
14 | 13 | ex 449 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) → ¬ 𝑉 FriendGrph 𝐸)) |