Proof of Theorem frgrncvvdeqlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frgrncvvdeq.f | . . . 4
⊢ (𝜑 → 𝐺 ∈ FriendGraph ) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺 ∈ FriendGraph ) | 
| 3 |  | frgrncvvdeq.nx | . . . . . . 7
⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) | 
| 4 | 3 | eleq2i 2833 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) | 
| 5 |  | frgrncvvdeq.v1 | . . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) | 
| 6 | 5 | nbgrisvtx 29358 | . . . . . . 7
⊢ (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉) | 
| 7 | 6 | a1i 11 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) | 
| 8 | 4, 7 | biimtrid 242 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉)) | 
| 9 | 8 | imp 406 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝑉) | 
| 10 |  | frgrncvvdeq.y | . . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑉) | 
| 11 | 10 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ 𝑉) | 
| 12 |  | frgrncvvdeq.xy | . . . . . 6
⊢ (𝜑 → 𝑌 ∉ 𝐷) | 
| 13 |  | elnelne2 3058 | . . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑌 ∉ 𝐷) → 𝑥 ≠ 𝑌) | 
| 14 | 13 | expcom 413 | . . . . . 6
⊢ (𝑌 ∉ 𝐷 → (𝑥 ∈ 𝐷 → 𝑥 ≠ 𝑌)) | 
| 15 | 12, 14 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ≠ 𝑌)) | 
| 16 | 15 | imp 406 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ≠ 𝑌) | 
| 17 | 9, 11, 16 | 3jca 1129 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌)) | 
| 18 |  | frgrncvvdeq.e | . . . 4
⊢ 𝐸 = (Edg‘𝐺) | 
| 19 | 5, 18 | frcond1 30285 | . . 3
⊢ (𝐺 ∈ FriendGraph →
((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌) → ∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) | 
| 20 | 2, 17, 19 | sylc 65 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) | 
| 21 |  | frgrusgr 30280 | . . . 4
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
USGraph) | 
| 22 |  | prex 5437 | . . . . . . . . . . . 12
⊢ {𝑥, 𝑦} ∈ V | 
| 23 |  | prex 5437 | . . . . . . . . . . . 12
⊢ {𝑦, 𝑌} ∈ V | 
| 24 | 22, 23 | prss 4820 | . . . . . . . . . . 11
⊢ (({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸) ↔ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) | 
| 25 |  | ancom 460 | . . . . . . . . . . 11
⊢ (({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑌} ∈ 𝐸) ↔ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) | 
| 26 | 24, 25 | bitr3i 277 | . . . . . . . . . 10
⊢ ({{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 ↔ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) | 
| 27 | 26 | anbi2i 623 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ (𝑦 ∈ 𝑉 ∧ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) | 
| 28 |  | usgrumgr 29198 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UMGraph) | 
| 29 | 5, 18 | umgrpredgv 29157 | . . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) | 
| 30 | 29 | simprd 495 | . . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑦} ∈ 𝐸) → 𝑦 ∈ 𝑉) | 
| 31 | 30 | ex 412 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ UMGraph → ({𝑥, 𝑦} ∈ 𝐸 → 𝑦 ∈ 𝑉)) | 
| 32 | 28, 31 | syl 17 | . . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → ({𝑥, 𝑦} ∈ 𝐸 → 𝑦 ∈ 𝑉)) | 
| 33 | 32 | adantld 490 | . . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → (({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) → 𝑦 ∈ 𝑉)) | 
| 34 | 33 | pm4.71rd 562 | . . . . . . . . 9
⊢ (𝐺 ∈ USGraph → (({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) ↔ (𝑦 ∈ 𝑉 ∧ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)))) | 
| 35 | 27, 34 | bitr4id 290 | . . . . . . . 8
⊢ (𝐺 ∈ USGraph → ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ ({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) | 
| 36 |  | frgrncvvdeq.ny | . . . . . . . . . . 11
⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) | 
| 37 | 36 | eleq2i 2833 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝑁 ↔ 𝑦 ∈ (𝐺 NeighbVtx 𝑌)) | 
| 38 | 18 | nbusgreledg 29370 | . . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑌) ↔ {𝑦, 𝑌} ∈ 𝐸)) | 
| 39 | 37, 38 | bitr2id 284 | . . . . . . . . 9
⊢ (𝐺 ∈ USGraph → ({𝑦, 𝑌} ∈ 𝐸 ↔ 𝑦 ∈ 𝑁)) | 
| 40 | 39 | anbi1d 631 | . . . . . . . 8
⊢ (𝐺 ∈ USGraph → (({𝑦, 𝑌} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) ↔ (𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) | 
| 41 | 35, 40 | bitrd 279 | . . . . . . 7
⊢ (𝐺 ∈ USGraph → ((𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ (𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) | 
| 42 | 41 | eubidv 2586 | . . . . . 6
⊢ (𝐺 ∈ USGraph →
(∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) ↔ ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) | 
| 43 | 42 | biimpd 229 | . . . . 5
⊢ (𝐺 ∈ USGraph →
(∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸) → ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸))) | 
| 44 |  | df-reu 3381 | . . . . 5
⊢
(∃!𝑦 ∈
𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 ↔ ∃!𝑦(𝑦 ∈ 𝑉 ∧ {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸)) | 
| 45 |  | df-reu 3381 | . . . . 5
⊢
(∃!𝑦 ∈
𝑁 {𝑥, 𝑦} ∈ 𝐸 ↔ ∃!𝑦(𝑦 ∈ 𝑁 ∧ {𝑥, 𝑦} ∈ 𝐸)) | 
| 46 | 43, 44, 45 | 3imtr4g 296 | . . . 4
⊢ (𝐺 ∈ USGraph →
(∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) | 
| 47 | 1, 21, 46 | 3syl 18 | . . 3
⊢ (𝜑 → (∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) | 
| 48 | 47 | adantr 480 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃!𝑦 ∈ 𝑉 {{𝑥, 𝑦}, {𝑦, 𝑌}} ⊆ 𝐸 → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) | 
| 49 | 20, 48 | mpd 15 | 1
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) |