| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | usgredg3.v | . . . 4
⊢ 𝑉 = (Vtx‘𝐺) | 
| 2 |  | usgredg3.e | . . . 4
⊢ 𝐸 = (iEdg‘𝐺) | 
| 3 | 1, 2 | usgredg3 29234 | . . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → ∃𝑥 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) | 
| 4 |  | eleq2 2829 | . . . . . . . 8
⊢ ((𝐸‘𝑋) = {𝑥, 𝑧} → (𝑌 ∈ (𝐸‘𝑋) ↔ 𝑌 ∈ {𝑥, 𝑧})) | 
| 5 | 4 | adantl 481 | . . . . . . 7
⊢ ((𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}) → (𝑌 ∈ (𝐸‘𝑋) ↔ 𝑌 ∈ {𝑥, 𝑧})) | 
| 6 | 5 | adantl 481 | . . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → (𝑌 ∈ (𝐸‘𝑋) ↔ 𝑌 ∈ {𝑥, 𝑧})) | 
| 7 |  | simplrr 777 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → 𝑧 ∈ 𝑉) | 
| 8 | 7 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑌 = 𝑥 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → 𝑧 ∈ 𝑉) | 
| 9 |  | preq2 4733 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → {𝑥, 𝑦} = {𝑥, 𝑧}) | 
| 10 | 9 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → ({𝑥, 𝑧} = {𝑥, 𝑦} ↔ {𝑥, 𝑧} = {𝑥, 𝑧})) | 
| 11 | 10 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑌 = 𝑥 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) ∧ 𝑦 = 𝑧) → ({𝑥, 𝑧} = {𝑥, 𝑦} ↔ {𝑥, 𝑧} = {𝑥, 𝑧})) | 
| 12 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝑌 = 𝑥 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → {𝑥, 𝑧} = {𝑥, 𝑧}) | 
| 13 | 8, 11, 12 | rspcedvd 3623 | . . . . . . . . . 10
⊢ ((𝑌 = 𝑥 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → ∃𝑦 ∈ 𝑉 {𝑥, 𝑧} = {𝑥, 𝑦}) | 
| 14 |  | simprr 772 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → (𝐸‘𝑋) = {𝑥, 𝑧}) | 
| 15 |  | preq1 4732 | . . . . . . . . . . . 12
⊢ (𝑌 = 𝑥 → {𝑌, 𝑦} = {𝑥, 𝑦}) | 
| 16 | 14, 15 | eqeqan12rd 2751 | . . . . . . . . . . 11
⊢ ((𝑌 = 𝑥 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → ((𝐸‘𝑋) = {𝑌, 𝑦} ↔ {𝑥, 𝑧} = {𝑥, 𝑦})) | 
| 17 | 16 | rexbidv 3178 | . . . . . . . . . 10
⊢ ((𝑌 = 𝑥 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → (∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦} ↔ ∃𝑦 ∈ 𝑉 {𝑥, 𝑧} = {𝑥, 𝑦})) | 
| 18 | 13, 17 | mpbird 257 | . . . . . . . . 9
⊢ ((𝑌 = 𝑥 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}) | 
| 19 | 18 | ex 412 | . . . . . . . 8
⊢ (𝑌 = 𝑥 → ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) | 
| 20 |  | simplrl 776 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → 𝑥 ∈ 𝑉) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑌 = 𝑧 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → 𝑥 ∈ 𝑉) | 
| 22 |  | preq2 4733 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → {𝑧, 𝑦} = {𝑧, 𝑥}) | 
| 23 | 22 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → ({𝑥, 𝑧} = {𝑧, 𝑦} ↔ {𝑥, 𝑧} = {𝑧, 𝑥})) | 
| 24 | 23 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑌 = 𝑧 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) ∧ 𝑦 = 𝑥) → ({𝑥, 𝑧} = {𝑧, 𝑦} ↔ {𝑥, 𝑧} = {𝑧, 𝑥})) | 
| 25 |  | prcom 4731 | . . . . . . . . . . . 12
⊢ {𝑥, 𝑧} = {𝑧, 𝑥} | 
| 26 | 25 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑌 = 𝑧 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → {𝑥, 𝑧} = {𝑧, 𝑥}) | 
| 27 | 21, 24, 26 | rspcedvd 3623 | . . . . . . . . . 10
⊢ ((𝑌 = 𝑧 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → ∃𝑦 ∈ 𝑉 {𝑥, 𝑧} = {𝑧, 𝑦}) | 
| 28 |  | preq1 4732 | . . . . . . . . . . . 12
⊢ (𝑌 = 𝑧 → {𝑌, 𝑦} = {𝑧, 𝑦}) | 
| 29 | 14, 28 | eqeqan12rd 2751 | . . . . . . . . . . 11
⊢ ((𝑌 = 𝑧 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → ((𝐸‘𝑋) = {𝑌, 𝑦} ↔ {𝑥, 𝑧} = {𝑧, 𝑦})) | 
| 30 | 29 | rexbidv 3178 | . . . . . . . . . 10
⊢ ((𝑌 = 𝑧 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → (∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦} ↔ ∃𝑦 ∈ 𝑉 {𝑥, 𝑧} = {𝑧, 𝑦})) | 
| 31 | 27, 30 | mpbird 257 | . . . . . . . . 9
⊢ ((𝑌 = 𝑧 ∧ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}))) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}) | 
| 32 | 31 | ex 412 | . . . . . . . 8
⊢ (𝑌 = 𝑧 → ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) | 
| 33 | 19, 32 | jaoi 857 | . . . . . . 7
⊢ ((𝑌 = 𝑥 ∨ 𝑌 = 𝑧) → ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) | 
| 34 |  | elpri 4648 | . . . . . . 7
⊢ (𝑌 ∈ {𝑥, 𝑧} → (𝑌 = 𝑥 ∨ 𝑌 = 𝑧)) | 
| 35 | 33, 34 | syl11 33 | . . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → (𝑌 ∈ {𝑥, 𝑧} → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) | 
| 36 | 6, 35 | sylbid 240 | . . . . 5
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧})) → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) | 
| 37 | 36 | ex 412 | . . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}) → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}))) | 
| 38 | 37 | rexlimdvva 3212 | . . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (∃𝑥 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑥 ≠ 𝑧 ∧ (𝐸‘𝑋) = {𝑥, 𝑧}) → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}))) | 
| 39 | 3, 38 | mpd 15 | . 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) | 
| 40 | 39 | 3impia 1117 | 1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}) |