Proof of Theorem 2pthfrgrarn
Step | Hyp | Ref
| Expression |
1 | | frisusgrapr 26518 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸)) |
2 | | reurex 3137 |
. . . . . . 7
⊢
(∃!𝑏 ∈
𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) |
3 | | prcom 4211 |
. . . . . . . . . . . 12
⊢ {𝑎, 𝑏} = {𝑏, 𝑎} |
4 | 3 | eleq1i 2679 |
. . . . . . . . . . 11
⊢ ({𝑎, 𝑏} ∈ ran 𝐸 ↔ {𝑏, 𝑎} ∈ ran 𝐸) |
5 | 4 | anbi1i 727 |
. . . . . . . . . 10
⊢ (({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ↔ ({𝑏, 𝑎} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |
6 | | zfpair2 4834 |
. . . . . . . . . . 11
⊢ {𝑏, 𝑎} ∈ V |
7 | | zfpair2 4834 |
. . . . . . . . . . 11
⊢ {𝑏, 𝑐} ∈ V |
8 | 6, 7 | prss 4291 |
. . . . . . . . . 10
⊢ (({𝑏, 𝑎} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ↔ {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) |
9 | 5, 8 | bitri 263 |
. . . . . . . . 9
⊢ (({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ↔ {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) |
10 | 9 | biimpri 217 |
. . . . . . . 8
⊢ ({{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |
11 | 10 | reximi 2994 |
. . . . . . 7
⊢
(∃𝑏 ∈
𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |
12 | 2, 11 | syl 17 |
. . . . . 6
⊢
(∃!𝑏 ∈
𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |
13 | 12 | a1i 11 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑐 ∈ (𝑉 ∖ {𝑎})) → (∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸))) |
14 | 13 | ralimdva 2945 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑎 ∈ 𝑉) → (∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸))) |
15 | 14 | ralimdva 2945 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸))) |
16 | 15 | imp 444 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |
17 | 1, 16 | syl 17 |
1
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) |