Proof of Theorem frgrncvvdeqlem3
Step | Hyp | Ref
| Expression |
1 | | frgrncvvdeq.f |
. . . 4
⊢ (𝜑 → 𝐺 ∈ FriendGraph ) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺 ∈ FriendGraph ) |
3 | | frgrncvvdeq.nx |
. . . . . . 7
⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) |
4 | 3 | eleq2i 2680 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) |
5 | | frgrusgr 41432 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
6 | | frgrncvvdeq.v1 |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
7 | 6 | nbgrisvtx 40581 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑥 ∈ 𝑉) |
8 | 7 | ex 449 |
. . . . . . 7
⊢ (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) |
9 | 1, 5, 8 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) |
10 | 4, 9 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉)) |
11 | 10 | imp 444 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝑉) |
12 | | frgrncvvdeq.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ 𝑉) |
14 | | frgrncvvdeq.e |
. . . . . 6
⊢ 𝐸 = (Edg‘𝐺) |
15 | | frgrncvvdeq.ny |
. . . . . 6
⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) |
16 | | frgrncvvdeq.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
17 | | frgrncvvdeq.ne |
. . . . . 6
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
18 | | frgrncvvdeq.xy |
. . . . . 6
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
19 | | frgrncvvdeq.a |
. . . . . 6
⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
20 | 6, 14, 3, 15, 16, 12, 17, 18, 1, 19 | frgrncvvdeqlem1 41469 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ (𝑉 ∖ {𝑥})) |
21 | | eldif 3550 |
. . . . . 6
⊢ (𝑌 ∈ (𝑉 ∖ {𝑥}) ↔ (𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ {𝑥})) |
22 | | vsnid 4156 |
. . . . . . . 8
⊢ 𝑥 ∈ {𝑥} |
23 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑌 = 𝑥 → (𝑌 ∈ {𝑥} ↔ 𝑥 ∈ {𝑥})) |
24 | 23 | eqcoms 2618 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝑌 ∈ {𝑥} ↔ 𝑥 ∈ {𝑥})) |
25 | 22, 24 | mpbiri 247 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → 𝑌 ∈ {𝑥}) |
26 | 25 | necon3bi 2808 |
. . . . . 6
⊢ (¬
𝑌 ∈ {𝑥} → 𝑥 ≠ 𝑌) |
27 | 21, 26 | simplbiim 657 |
. . . . 5
⊢ (𝑌 ∈ (𝑉 ∖ {𝑥}) → 𝑥 ≠ 𝑌) |
28 | 20, 27 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ≠ 𝑌) |
29 | 11, 13, 28 | 3jca 1235 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌)) |
30 | 6, 14 | frcond1 41438 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌) → ∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) |
31 | 2, 29, 30 | sylc 63 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) |
32 | | prex 4836 |
. . . . . . . . . . . 12
⊢ {𝑥, 𝑦} ∈ V |
33 | | prex 4836 |
. . . . . . . . . . . 12
⊢ {𝑦, 𝑌} ∈ V |
34 | 32, 33 | prss 4291 |
. . . . . . . . . . 11
⊢ (({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸) ↔ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) |
35 | | simpr 476 |
. . . . . . . . . . 11
⊢ (({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸) → {𝑦, 𝑌} ∈ 𝐸) |
36 | 34, 35 | sylbir 224 |
. . . . . . . . . 10
⊢ ({{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → {𝑦, 𝑌} ∈ 𝐸) |
37 | 36 | ad2antll 761 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) → {𝑦, 𝑌} ∈ 𝐸) |
38 | 15 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 = (𝐺 NeighbVtx 𝑌)) |
39 | 38 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝑁 ↔ 𝑦 ∈ (𝐺 NeighbVtx 𝑌))) |
40 | 14 | nbusgreledg 40575 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑌) ↔ {𝑦, 𝑌} ∈ 𝐸)) |
41 | 1, 5, 40 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ (𝐺 NeighbVtx 𝑌) ↔ {𝑦, 𝑌} ∈ 𝐸)) |
42 | 39, 41 | bitrd 267 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑁 ↔ {𝑦, 𝑌} ∈ 𝐸)) |
43 | 42 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑦 ∈ 𝑁 ↔ {𝑦, 𝑌} ∈ 𝐸)) |
44 | 43 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) → (𝑦 ∈ 𝑁 ↔ {𝑦, 𝑌} ∈ 𝐸)) |
45 | 37, 44 | mpbird 246 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) → 𝑦 ∈ 𝑁) |
46 | | simpl 472 |
. . . . . . . . . 10
⊢ (({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸) → {𝑥, 𝑦} ∈ 𝐸) |
47 | 34, 46 | sylbir 224 |
. . . . . . . . 9
⊢ ({{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → {𝑥, 𝑦} ∈ 𝐸) |
48 | 47 | ad2antll 761 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) → {𝑥, 𝑦} ∈ 𝐸) |
49 | 45, 48 | jca 553 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) → (𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸)) |
50 | 49 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) → (𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
51 | 15 | eleq2i 2680 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑁 ↔ 𝑦 ∈ (𝐺 NeighbVtx 𝑌)) |
52 | 51, 41 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝑁 ↔ {𝑦, 𝑌} ∈ 𝐸)) |
53 | 52 | biimpd 218 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑁 → {𝑦, 𝑌} ∈ 𝐸)) |
54 | 53 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑦 ∈ 𝑁 → {𝑦, 𝑌} ∈ 𝐸)) |
55 | 54 | impcom 445 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → {𝑦, 𝑌} ∈ 𝐸) |
56 | 6 | nbgrisvtx 40581 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ USGraph ∧ 𝑦 ∈ (𝐺 NeighbVtx 𝑌)) → 𝑦 ∈ 𝑉) |
57 | 56 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑌) → 𝑦 ∈ 𝑉)) |
58 | 1, 5, 57 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ (𝐺 NeighbVtx 𝑌) → 𝑦 ∈ 𝑉)) |
59 | 51, 58 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ 𝑁 → 𝑦 ∈ 𝑉)) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑦 ∈ 𝑁 → 𝑦 ∈ 𝑉)) |
61 | 60 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → 𝑦 ∈ 𝑉) |
62 | 61 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((({𝑦, 𝑌} ∈ 𝐸 ∧ (𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷))) ∧ {𝑥, 𝑦} ∈ 𝐸) → 𝑦 ∈ 𝑉) |
63 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ (({𝑦, 𝑌} ∈ 𝐸 ∧ (𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷))) → {𝑦, 𝑌} ∈ 𝐸) |
64 | | id 22 |
. . . . . . . . . . . . 13
⊢ ({𝑥, 𝑦} ∈ 𝐸 → {𝑥, 𝑦} ∈ 𝐸) |
65 | 63, 64 | anim12ci 589 |
. . . . . . . . . . . 12
⊢ ((({𝑦, 𝑌} ∈ 𝐸 ∧ (𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷))) ∧ {𝑥, 𝑦} ∈ 𝐸) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸)) |
66 | 65, 34 | sylib 207 |
. . . . . . . . . . 11
⊢ ((({𝑦, 𝑌} ∈ 𝐸 ∧ (𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷))) ∧ {𝑥, 𝑦} ∈ 𝐸) → {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) |
67 | 62, 66 | jca 553 |
. . . . . . . . . 10
⊢ ((({𝑦, 𝑌} ∈ 𝐸 ∧ (𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷))) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) |
68 | 67 | ex 449 |
. . . . . . . . 9
⊢ (({𝑦, 𝑌} ∈ 𝐸 ∧ (𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷))) → ({𝑥, 𝑦} ∈ 𝐸 → (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸))) |
69 | 55, 68 | mpancom 700 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑁 ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → ({𝑥, 𝑦} ∈ 𝐸 → (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸))) |
70 | 69 | impancom 455 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸))) |
71 | 70 | com12 32 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸))) |
72 | 50, 71 | impbid 201 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ (𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
73 | 72 | eubidv 2478 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
74 | 73 | biimpd 218 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) → ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
75 | | df-reu 2903 |
. . 3
⊢
(∃!𝑦 ∈
𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 ↔ ∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) |
76 | | df-reu 2903 |
. . 3
⊢
(∃!𝑦 ∈
𝑁 {𝑥, 𝑦} ∈ 𝐸 ↔ ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸)) |
77 | 74, 75, 76 | 3imtr4g 284 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
78 | 31, 77 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) |