This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgredgprvALT

Description: Alternate proof of usgredgprv , using usgredg2 instead of umgredgprv . (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 16-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses usgredg2.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
usgredgprv.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion usgredgprvALT ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 usgredg2.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2 usgredgprv.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 1 2 usgrss ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 )
4 1 usgredg2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 )
5 sseq1 ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) )
6 fveq2 ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = ( ♯ ‘ { 𝑀 , 𝑁 } ) )
7 6 eqeq1d ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
8 5 7 anbi12d ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) ↔ ( { 𝑀 , 𝑁 } ⊆ 𝑉 ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) ) )
9 eqid ⊢ { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 }
10 9 hashprdifel ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) )
11 prssg ⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) )
12 11 3adant3 ⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) )
13 12 biimprd ⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) → ( { 𝑀 , 𝑁 } ⊆ 𝑉 → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
14 10 13 syl ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( { 𝑀 , 𝑁 } ⊆ 𝑉 → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
15 14 impcom ⊢ ( ( { 𝑀 , 𝑁 } ⊆ 𝑉 ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
16 8 15 biimtrdi ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
17 16 com12 ⊢ ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
18 3 4 17 syl2anc ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )