Step | Hyp | Ref
| Expression |
1 | | frisusgrapr 26518 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸)) |
2 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴}) |
3 | 2 | difeq2d 3690 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑉 ∖ {𝑎}) = (𝑉 ∖ {𝐴})) |
4 | | preq2 4213 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → {𝑏, 𝑎} = {𝑏, 𝐴}) |
5 | 4 | preq1d 4218 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → {{𝑏, 𝑎}, {𝑏, 𝑐}} = {{𝑏, 𝐴}, {𝑏, 𝑐}}) |
6 | 5 | sseq1d 3595 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → ({{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸)) |
7 | 6 | reubidv 3103 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ ∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸)) |
8 | 3, 7 | raleqbidv 3129 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸)) |
9 | 8 | rspcva 3280 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸) |
10 | | elsni 4142 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴) |
11 | 10 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶) |
12 | 11 | necon3ai 2807 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ 𝐶 → ¬ 𝐶 ∈ {𝐴}) |
13 | 12 | anim2i 591 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → (𝐶 ∈ 𝑉 ∧ ¬ 𝐶 ∈ {𝐴})) |
14 | | eldif 3550 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑉 ∖ {𝐴}) ↔ (𝐶 ∈ 𝑉 ∧ ¬ 𝐶 ∈ {𝐴})) |
15 | 13, 14 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → 𝐶 ∈ (𝑉 ∖ {𝐴})) |
16 | | preq2 4213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝐶 → {𝑏, 𝑐} = {𝑏, 𝐶}) |
17 | 16 | preq2d 4219 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝐶 → {{𝑏, 𝐴}, {𝑏, 𝑐}} = {{𝑏, 𝐴}, {𝑏, 𝐶}}) |
18 | 17 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝐶 → ({{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |
19 | 18 | reubidv 3103 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝐶 → (∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ ∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |
20 | 19 | rspcva 3280 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ (𝑉 ∖ {𝐴}) ∧ ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸) |
21 | | prcom 4211 |
. . . . . . . . . . . . . . . 16
⊢ {𝑏, 𝐴} = {𝐴, 𝑏} |
22 | 21 | preq1i 4215 |
. . . . . . . . . . . . . . 15
⊢ {{𝑏, 𝐴}, {𝑏, 𝐶}} = {{𝐴, 𝑏}, {𝑏, 𝐶}} |
23 | 22 | sseq1i 3592 |
. . . . . . . . . . . . . 14
⊢ ({{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸 ↔ {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸) |
24 | 23 | reubii 3105 |
. . . . . . . . . . . . 13
⊢
(∃!𝑏 ∈
𝑉 {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸 ↔ ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸) |
25 | 20, 24 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (𝑉 ∖ {𝐴}) ∧ ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸) |
26 | 25 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑉 ∖ {𝐴}) → (∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |
27 | 15, 26 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → (∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |
28 | 27 | ex 449 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → (𝐴 ≠ 𝐶 → (∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))) |
29 | 28 | com13 86 |
. . . . . . . 8
⊢
(∀𝑐 ∈
(𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → (𝐴 ≠ 𝐶 → (𝐶 ∈ 𝑉 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))) |
30 | 9, 29 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) → (𝐴 ≠ 𝐶 → (𝐶 ∈ 𝑉 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))) |
31 | 30 | ex 449 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → (𝐴 ≠ 𝐶 → (𝐶 ∈ 𝑉 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)))) |
32 | 31 | com24 93 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐶 ∈ 𝑉 → (𝐴 ≠ 𝐶 → (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)))) |
33 | 32 | 3imp 1249 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |
34 | 33 | com12 32 |
. . 3
⊢
(∀𝑎 ∈
𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |
35 | 34 | adantl 481 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |
36 | 1, 35 | syl 17 |
1
⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)) |