Proof of Theorem frgrncvvdeqlem2
Step | Hyp | Ref
| Expression |
1 | | frgrncvvdeq.f |
. . . 4
⊢ (𝜑 → 𝐺 ∈ FriendGraph ) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺 ∈ FriendGraph ) |
3 | | frgrncvvdeq.nx |
. . . . . . 7
⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) |
4 | 3 | eleq2i 2693 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) |
5 | | frgrusgr 27124 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
6 | | frgrncvvdeq.v1 |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
7 | 6 | nbgrisvtx 26255 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑥 ∈ 𝑉) |
8 | 7 | ex 450 |
. . . . . . 7
⊢ (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) |
9 | 1, 5, 8 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) |
10 | 4, 9 | syl5bi 232 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉)) |
11 | 10 | imp 445 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝑉) |
12 | | frgrncvvdeq.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
13 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ 𝑉) |
14 | | frgrncvvdeq.xy |
. . . . . 6
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
15 | | elnelne2 2908 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑌 ∉ 𝐷) → 𝑥 ≠ 𝑌) |
16 | 15 | expcom 451 |
. . . . . 6
⊢ (𝑌 ∉ 𝐷 → (𝑥 ∈ 𝐷 → 𝑥 ≠ 𝑌)) |
17 | 14, 16 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ≠ 𝑌)) |
18 | 17 | imp 445 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ≠ 𝑌) |
19 | 11, 13, 18 | 3jca 1242 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌)) |
20 | | frgrncvvdeq.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
21 | 6, 20 | frcond1 27130 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌) → ∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) |
22 | 2, 19, 21 | sylc 65 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) |
23 | | usgrumgr 26074 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph
) |
24 | 6, 20 | umgrpredgv 26035 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) |
25 | 24 | simprd 479 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑦} ∈ 𝐸) → 𝑦 ∈ 𝑉) |
26 | 25 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ UMGraph → ({𝑥, 𝑦} ∈ 𝐸 → 𝑦 ∈ 𝑉)) |
27 | 23, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → ({𝑥, 𝑦} ∈ 𝐸 → 𝑦 ∈ 𝑉)) |
28 | 27 | adantld 483 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → (({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) → 𝑦 ∈ 𝑉)) |
29 | 28 | pm4.71rd 667 |
. . . . . . . . 9
⊢ (𝐺 ∈ USGraph → (({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) ↔ (𝑦 ∈ 𝑉 ∧ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)))) |
30 | | prex 4909 |
. . . . . . . . . . . 12
⊢ {𝑥, 𝑦} ∈ V |
31 | | prex 4909 |
. . . . . . . . . . . 12
⊢ {𝑦, 𝑌} ∈ V |
32 | 30, 31 | prss 4351 |
. . . . . . . . . . 11
⊢ (({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸) ↔ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) |
33 | | ancom 466 |
. . . . . . . . . . 11
⊢ (({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸) ↔ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) |
34 | 32, 33 | bitr3i 266 |
. . . . . . . . . 10
⊢ ({{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 ↔ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) |
35 | 34 | anbi2i 730 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ (𝑦 ∈ 𝑉 ∧ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
36 | 29, 35 | syl6rbbr 279 |
. . . . . . . 8
⊢ (𝐺 ∈ USGraph → ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
37 | | frgrncvvdeq.ny |
. . . . . . . . . . 11
⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) |
38 | 37 | eleq2i 2693 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑁 ↔ 𝑦 ∈ (𝐺 NeighbVtx 𝑌)) |
39 | 20 | nbusgreledg 26249 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑌) ↔ {𝑦, 𝑌} ∈ 𝐸)) |
40 | 38, 39 | syl5rbb 273 |
. . . . . . . . 9
⊢ (𝐺 ∈ USGraph → ({𝑦, 𝑌} ∈ 𝐸 ↔ 𝑦 ∈ 𝑁)) |
41 | 40 | anbi1d 741 |
. . . . . . . 8
⊢ (𝐺 ∈ USGraph → (({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) ↔ (𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
42 | 36, 41 | bitrd 268 |
. . . . . . 7
⊢ (𝐺 ∈ USGraph → ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ (𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
43 | 42 | eubidv 2490 |
. . . . . 6
⊢ (𝐺 ∈ USGraph →
(∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
44 | 43 | biimpd 219 |
. . . . 5
⊢ (𝐺 ∈ USGraph →
(∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) → ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
45 | | df-reu 2919 |
. . . . 5
⊢
(∃!𝑦 ∈
𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 ↔ ∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) |
46 | | df-reu 2919 |
. . . . 5
⊢
(∃!𝑦 ∈
𝑁 {𝑥, 𝑦} ∈ 𝐸 ↔ ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸)) |
47 | 44, 45, 46 | 3imtr4g 285 |
. . . 4
⊢ (𝐺 ∈ USGraph →
(∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
48 | 1, 5, 47 | 3syl 18 |
. . 3
⊢ (𝜑 → (∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
49 | 48 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
50 | 22, 49 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) |