Metamath Proof Explorer

Theorem frgrwopreglem5lem

Description: Lemma for frgrwopreglem5 . (Contributed by AV, 5-Feb-2022)

Ref Expression
Hypotheses frgrwopreg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
frgrwopreg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion frgrwopreglem5lem ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ∧ ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3 frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
4 frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
5 frgrwopreg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
6 3 rabeq2i ⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) )
7 fveqeq2 ⊢ ( 𝑥 = 𝑎 → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ( 𝐷 ‘ 𝑎 ) = 𝐾 ) )
8 7 3 elrab2 ⊢ ( 𝑎 ∈ 𝐴 ↔ ( 𝑎 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑎 ) = 𝐾 ) )
9 eqtr3 ⊢ ( ( ( 𝐷 ‘ 𝑎 ) = 𝐾 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) )
10 9 expcom ⊢ ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ) )
11 10 adantl ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ) )
12 11 com12 ⊢ ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ) )
13 8 12 simplbiim ⊢ ( 𝑎 ∈ 𝐴 → ( ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ) )
14 6 13 syl5bi ⊢ ( 𝑎 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ) )
15 14 imp ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) )
16 15 adantr ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) )
17 1 2 3 4 frgrwopreglem3 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) )
18 17 ad2ant2r ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) )
19 fveqeq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ( 𝐷 ‘ 𝑧 ) = 𝐾 ) )
20 19 cbvrabv ⊢ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = { 𝑧 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑧 ) = 𝐾 }
21 3 20 eqtri ⊢ 𝐴 = { 𝑧 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑧 ) = 𝐾 }
22 1 2 21 4 frgrwopreglem3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) )
23 22 ad2ant2l ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) )
24 16 18 23 3jca ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ∧ ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) ) )