Theorem frgrwopreglem3

Description: Lemma 3 for frgrwopreg . The vertices in the sets A and B have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 2-Jan-2022)

	Ref	Expression
Hypotheses	frgrwopreg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
	frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
	frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
Assertion	frgrwopreglem3	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		frgrwopreg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3		frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
4		frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
5		fveqeq2	⊢ ( 𝑥 = 𝑌 → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ( 𝐷 ‘ 𝑌 ) = 𝐾 ) )
6	5	notbid	⊢ ( 𝑥 = 𝑌 → ( ¬ ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ¬ ( 𝐷 ‘ 𝑌 ) = 𝐾 ) )
7	3	difeq2i	⊢ ( 𝑉 ∖ 𝐴 ) = ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } )
8		notrab	⊢ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = { 𝑥 ∈ 𝑉 ∣ ¬ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
9	4 7 8	3eqtri	⊢ 𝐵 = { 𝑥 ∈ 𝑉 ∣ ¬ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
10	6 9	elrab2	⊢ ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑉 ∧ ¬ ( 𝐷 ‘ 𝑌 ) = 𝐾 ) )
11		fveqeq2	⊢ ( 𝑥 = 𝑋 → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ( 𝐷 ‘ 𝑋 ) = 𝐾 ) )
12	11 3	elrab2	⊢ ( 𝑋 ∈ 𝐴 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑋 ) = 𝐾 ) )
13		eqeq2	⊢ ( ( 𝐷 ‘ 𝑋 ) = 𝐾 → ( ( 𝐷 ‘ 𝑌 ) = ( 𝐷 ‘ 𝑋 ) ↔ ( 𝐷 ‘ 𝑌 ) = 𝐾 ) )
14	13	notbid	⊢ ( ( 𝐷 ‘ 𝑋 ) = 𝐾 → ( ¬ ( 𝐷 ‘ 𝑌 ) = ( 𝐷 ‘ 𝑋 ) ↔ ¬ ( 𝐷 ‘ 𝑌 ) = 𝐾 ) )
15		neqne	⊢ ( ¬ ( 𝐷 ‘ 𝑌 ) = ( 𝐷 ‘ 𝑋 ) → ( 𝐷 ‘ 𝑌 ) ≠ ( 𝐷 ‘ 𝑋 ) )
16	15	necomd	⊢ ( ¬ ( 𝐷 ‘ 𝑌 ) = ( 𝐷 ‘ 𝑋 ) → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) )
17	14 16	syl6bir	⊢ ( ( 𝐷 ‘ 𝑋 ) = 𝐾 → ( ¬ ( 𝐷 ‘ 𝑌 ) = 𝐾 → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) )
18	12 17	simplbiim	⊢ ( 𝑋 ∈ 𝐴 → ( ¬ ( 𝐷 ‘ 𝑌 ) = 𝐾 → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) )
19	18	com12	⊢ ( ¬ ( 𝐷 ‘ 𝑌 ) = 𝐾 → ( 𝑋 ∈ 𝐴 → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) )
20	10 19	simplbiim	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑋 ∈ 𝐴 → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) )
21	20	impcom	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) )