Metamath Proof Explorer

Theorem usgredg4

Description: For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 17-Oct-2020)

Ref Expression
Hypotheses usgredg3.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgredg3.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion usgredg4 ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ ( 𝐸 ‘ 𝑋 ) ) → ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } )

Proof

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