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	syl6bi	⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
17	16	com12	⊢ ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
18	3 4 17	syl2anc	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )