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