Metamath Proof Explorer

Theorem frgrwopreglem5lem

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

Ref Expression
Hypotheses frgrwopreg.v ⊢ V = Vtx ⁡ G
frgrwopreg.d ⊢ D = VtxDeg ⁡ G
frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
frgrwopreg.b ⊢ B = V ∖ A
frgrwopreg.e ⊢ E = Edg ⁡ G
Assertion frgrwopreglem5lem ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → D ⁡ a = D ⁡ x ∧ D ⁡ a ≠ D ⁡ b ∧ D ⁡ x ≠ D ⁡ y

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢ V = Vtx ⁡ G
2 frgrwopreg.d ⊢ D = VtxDeg ⁡ G
3 frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
4 frgrwopreg.b ⊢ B = V ∖ A
5 frgrwopreg.e ⊢ E = Edg ⁡ G
6 3 rabeq2i ⊢ x ∈ A ↔ x ∈ V ∧ D ⁡ x = K
7 fveqeq2 ⊢ x = a → D ⁡ x = K ↔ D ⁡ a = K
8 7 3 elrab2 ⊢ a ∈ A ↔ a ∈ V ∧ D ⁡ a = K
9 eqtr3 ⊢ D ⁡ a = K ∧ D ⁡ x = K → D ⁡ a = D ⁡ x
10 9 expcom ⊢ D ⁡ x = K → D ⁡ a = K → D ⁡ a = D ⁡ x
11 10 adantl ⊢ x ∈ V ∧ D ⁡ x = K → D ⁡ a = K → D ⁡ a = D ⁡ x
12 11 com12 ⊢ D ⁡ a = K → x ∈ V ∧ D ⁡ x = K → D ⁡ a = D ⁡ x
13 8 12 simplbiim ⊢ a ∈ A → x ∈ V ∧ D ⁡ x = K → D ⁡ a = D ⁡ x
14 6 13 syl5bi ⊢ a ∈ A → x ∈ A → D ⁡ a = D ⁡ x
15 14 imp ⊢ a ∈ A ∧ x ∈ A → D ⁡ a = D ⁡ x
16 15 adantr ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → D ⁡ a = D ⁡ x
17 1 2 3 4 frgrwopreglem3 ⊢ a ∈ A ∧ b ∈ B → D ⁡ a ≠ D ⁡ b
18 17 ad2ant2r ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → D ⁡ a ≠ D ⁡ b
19 fveqeq2 ⊢ x = z → D ⁡ x = K ↔ D ⁡ z = K
20 19 cbvrabv ⊢ x ∈ V | D ⁡ x = K = z ∈ V | D ⁡ z = K
21 3 20 eqtri ⊢ A = z ∈ V | D ⁡ z = K
22 1 2 21 4 frgrwopreglem3 ⊢ x ∈ A ∧ y ∈ B → D ⁡ x ≠ D ⁡ y
23 22 ad2ant2l ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → D ⁡ x ≠ D ⁡ y
24 16 18 23 3jca ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → D ⁡ a = D ⁡ x ∧ D ⁡ a ≠ D ⁡ b ∧ D ⁡ x ≠ D ⁡ y