Proof of Theorem dfsclnbgr6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) → 𝑛 ∈ 𝑒) | 
| 2 | 1 | anim1i 615 | . . . . . . . . . 10
⊢ (((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∧ 𝑛 = 𝑁) → (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)) | 
| 3 | 2 | olcd 874 | . . . . . . . . 9
⊢ (((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∧ 𝑛 = 𝑁) → (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁))) | 
| 4 | 3 | expcom 413 | . . . . . . . 8
⊢ (𝑛 = 𝑁 → ((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) → (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)))) | 
| 5 |  | 3anass 1094 | . . . . . . . . . . . 12
⊢ ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ↔ (𝑛 ≠ 𝑁 ∧ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) | 
| 6 | 5 | biimpri 228 | . . . . . . . . . . 11
⊢ ((𝑛 ≠ 𝑁 ∧ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)) → (𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)) | 
| 7 | 6 | orcd 873 | . . . . . . . . . 10
⊢ ((𝑛 ≠ 𝑁 ∧ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)) → ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))) | 
| 8 | 7 | orcd 873 | . . . . . . . . 9
⊢ ((𝑛 ≠ 𝑁 ∧ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)) → (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁))) | 
| 9 | 8 | ex 412 | . . . . . . . 8
⊢ (𝑛 ≠ 𝑁 → ((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) → (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)))) | 
| 10 | 4, 9 | pm2.61ine 3024 | . . . . . . 7
⊢ ((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) → (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁))) | 
| 11 |  | 3simpc 1150 | . . . . . . . . . 10
⊢ ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)) | 
| 12 | 11 | a1i 11 | . . . . . . . . 9
⊢ (𝑁 ∈ 𝑉 → ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) | 
| 13 |  | vsnid 4662 | . . . . . . . . . . . . . . . 16
⊢ 𝑛 ∈ {𝑛} | 
| 14 | 13 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑒 = {𝑛} → 𝑛 ∈ {𝑛}) | 
| 15 |  | eleq2 2829 | . . . . . . . . . . . . . . 15
⊢ (𝑒 = {𝑛} → (𝑛 ∈ 𝑒 ↔ 𝑛 ∈ {𝑛})) | 
| 16 | 14, 15 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (𝑒 = {𝑛} → 𝑛 ∈ 𝑒) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑛 = 𝑁 ∧ 𝑒 = {𝑛}) → 𝑛 ∈ 𝑒) | 
| 18 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑁 → (𝑛 ∈ 𝑒 ↔ 𝑁 ∈ 𝑒)) | 
| 19 | 18 | bicomd 223 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → (𝑁 ∈ 𝑒 ↔ 𝑛 ∈ 𝑒)) | 
| 20 | 19 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑛 = 𝑁 ∧ 𝑒 = {𝑛}) → (𝑁 ∈ 𝑒 ↔ 𝑛 ∈ 𝑒)) | 
| 21 | 17, 20 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝑛 = 𝑁 ∧ 𝑒 = {𝑛}) → 𝑁 ∈ 𝑒) | 
| 22 | 21 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) → 𝑁 ∈ 𝑒) | 
| 23 | 17 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) → 𝑛 ∈ 𝑒) | 
| 24 | 22, 23 | jca 511 | . . . . . . . . . 10
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)) | 
| 25 | 24 | ex 412 | . . . . . . . . 9
⊢ (𝑁 ∈ 𝑉 → ((𝑛 = 𝑁 ∧ 𝑒 = {𝑛}) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) | 
| 26 | 12, 25 | jaod 859 | . . . . . . . 8
⊢ (𝑁 ∈ 𝑉 → (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) | 
| 27 | 18 | biimpac 478 | . . . . . . . . . 10
⊢ ((𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁) → 𝑁 ∈ 𝑒) | 
| 28 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁) → 𝑛 ∈ 𝑒) | 
| 29 | 27, 28 | jca 511 | . . . . . . . . 9
⊢ ((𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)) | 
| 30 | 29 | a1i 11 | . . . . . . . 8
⊢ (𝑁 ∈ 𝑉 → ((𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) | 
| 31 | 26, 30 | jaod 859 | . . . . . . 7
⊢ (𝑁 ∈ 𝑉 → ((((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)) → (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) | 
| 32 | 10, 31 | impbid2 226 | . . . . . 6
⊢ (𝑁 ∈ 𝑉 → ((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ↔ (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)))) | 
| 33 | 32 | rexbidv 3178 | . . . . 5
⊢ (𝑁 ∈ 𝑉 → (∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ↔ ∃𝑒 ∈ 𝐸 (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)))) | 
| 34 |  | r19.43 3121 | . . . . . 6
⊢
(∃𝑒 ∈
𝐸 (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)) ↔ (∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ ∃𝑒 ∈ 𝐸 (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁))) | 
| 35 | 34 | a1i 11 | . . . . 5
⊢ (𝑁 ∈ 𝑉 → (∃𝑒 ∈ 𝐸 (((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)) ↔ (∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ ∃𝑒 ∈ 𝐸 (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)))) | 
| 36 |  | r19.41v 3188 | . . . . . . . 8
⊢
(∃𝑒 ∈
𝐸 (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁) ↔ (∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)) | 
| 37 | 36 | biancomi 462 | . . . . . . 7
⊢
(∃𝑒 ∈
𝐸 (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁) ↔ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒)) | 
| 38 | 37 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈ 𝑉 → (∃𝑒 ∈ 𝐸 (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁) ↔ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒))) | 
| 39 | 38 | orbi2d 915 | . . . . 5
⊢ (𝑁 ∈ 𝑉 → ((∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ ∃𝑒 ∈ 𝐸 (𝑛 ∈ 𝑒 ∧ 𝑛 = 𝑁)) ↔ (∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒)))) | 
| 40 | 33, 35, 39 | 3bitrd 305 | . . . 4
⊢ (𝑁 ∈ 𝑉 → (∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ↔ (∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒)))) | 
| 41 | 40 | rabbidv 3443 | . . 3
⊢ (𝑁 ∈ 𝑉 → {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)} = {𝑛 ∈ 𝑉 ∣ (∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒))}) | 
| 42 |  | unrab 4314 | . . . 4
⊢ ({𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))} ∪ {𝑛 ∈ 𝑉 ∣ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒)}) = {𝑛 ∈ 𝑉 ∣ (∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒))} | 
| 43 |  | rabsneq 4643 | . . . . . 6
⊢ (𝑁 ∈ 𝑉 → {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒} = {𝑛 ∈ 𝑉 ∣ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒)}) | 
| 44 | 43 | eqcomd 2742 | . . . . 5
⊢ (𝑁 ∈ 𝑉 → {𝑛 ∈ 𝑉 ∣ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒)} = {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒}) | 
| 45 | 44 | uneq2d 4167 | . . . 4
⊢ (𝑁 ∈ 𝑉 → ({𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))} ∪ {𝑛 ∈ 𝑉 ∣ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒)}) = ({𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))} ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒})) | 
| 46 | 42, 45 | eqtr3id 2790 | . . 3
⊢ (𝑁 ∈ 𝑉 → {𝑛 ∈ 𝑉 ∣ (∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) ∨ (𝑛 = 𝑁 ∧ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒))} = ({𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))} ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒})) | 
| 47 | 41, 46 | eqtrd 2776 | . 2
⊢ (𝑁 ∈ 𝑉 → {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)} = ({𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))} ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒})) | 
| 48 |  | dfvopnbgr2.v | . . 3
⊢ 𝑉 = (Vtx‘𝐺) | 
| 49 |  | dfsclnbgr6.s | . . 3
⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} | 
| 50 |  | dfvopnbgr2.e | . . 3
⊢ 𝐸 = (Edg‘𝐺) | 
| 51 | 48, 49, 50 | dfsclnbgr2 47837 | . 2
⊢ (𝑁 ∈ 𝑉 → 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)}) | 
| 52 |  | dfvopnbgr2.u | . . . 4
⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} | 
| 53 | 48, 50, 52 | dfvopnbgr2 47844 | . . 3
⊢ (𝑁 ∈ 𝑉 → 𝑈 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))}) | 
| 54 | 53 | uneq1d 4166 | . 2
⊢ (𝑁 ∈ 𝑉 → (𝑈 ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒}) = ({𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))} ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒})) | 
| 55 | 47, 51, 54 | 3eqtr4d 2786 | 1
⊢ (𝑁 ∈ 𝑉 → 𝑆 = (𝑈 ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒})) |