Metamath Proof Explorer

Theorem frgrwopreglem5ALT

Description: Alternate direct proof of frgrwopreglem5 , not using frgrwopreglem5a . This proof would be even a little bit shorter than the proof of frgrwopreglem5 without using frgrwopreglem5lem . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 3-Jan-2022) (Proof shortened by AV, 5-Feb-2022) (New usage is discouraged.) (Proof modification is discouraged.)

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 frgrwopreglem5ALT ⊢ G ∈ FriendGraph ∧ 1 < A ∧ 1 < B → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E

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 simpllr ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a ≠ x
7 6 anim1i ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ b ≠ y → a ≠ x ∧ b ≠ y
8 1 2 3 4 5 frgrwopreglem4 ⊢ G ∈ FriendGraph → ∀ z ∈ A ∀ b ∈ B z b ∈ E
9 preq1 ⊢ z = a → z b = a b
10 9 eleq1d ⊢ z = a → z b ∈ E ↔ a b ∈ E
11 10 ralbidv ⊢ z = a → ∀ b ∈ B z b ∈ E ↔ ∀ b ∈ B a b ∈ E
12 11 cbvralvw ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E ↔ ∀ a ∈ A ∀ b ∈ B a b ∈ E
13 rsp2 ⊢ ∀ a ∈ A ∀ b ∈ B a b ∈ E → a ∈ A ∧ b ∈ B → a b ∈ E
14 13 com12 ⊢ a ∈ A ∧ b ∈ B → ∀ a ∈ A ∀ b ∈ B a b ∈ E → a b ∈ E
15 14 ad2ant2r ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → ∀ a ∈ A ∀ b ∈ B a b ∈ E → a b ∈ E
16 12 15 biimtrid ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → ∀ z ∈ A ∀ b ∈ B z b ∈ E → a b ∈ E
17 16 imp ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ ∀ z ∈ A ∀ b ∈ B z b ∈ E → a b ∈ E
18 prcom ⊢ b x = x b
19 preq1 ⊢ z = x → z b = x b
20 19 eleq1d ⊢ z = x → z b ∈ E ↔ x b ∈ E
21 20 ralbidv ⊢ z = x → ∀ b ∈ B z b ∈ E ↔ ∀ b ∈ B x b ∈ E
22 21 cbvralvw ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E ↔ ∀ x ∈ A ∀ b ∈ B x b ∈ E
23 rsp2 ⊢ ∀ x ∈ A ∀ b ∈ B x b ∈ E → x ∈ A ∧ b ∈ B → x b ∈ E
24 22 23 sylbi ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E → x ∈ A ∧ b ∈ B → x b ∈ E
25 24 com12 ⊢ x ∈ A ∧ b ∈ B → ∀ z ∈ A ∀ b ∈ B z b ∈ E → x b ∈ E
26 25 ad2ant2lr ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → ∀ z ∈ A ∀ b ∈ B z b ∈ E → x b ∈ E
27 26 imp ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ ∀ z ∈ A ∀ b ∈ B z b ∈ E → x b ∈ E
28 18 27 eqeltrid ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ ∀ z ∈ A ∀ b ∈ B z b ∈ E → b x ∈ E
29 17 28 jca ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ ∀ z ∈ A ∀ b ∈ B z b ∈ E → a b ∈ E ∧ b x ∈ E
30 29 expcom ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E → a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a b ∈ E ∧ b x ∈ E
31 8 30 syl ⊢ G ∈ FriendGraph → a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a b ∈ E ∧ b x ∈ E
32 31 adantr ⊢ G ∈ FriendGraph ∧ a ≠ x → a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a b ∈ E ∧ b x ∈ E
33 32 impl ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a b ∈ E ∧ b x ∈ E
34 33 adantr ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ b ≠ y → a b ∈ E ∧ b x ∈ E
35 preq2 ⊢ b = y → x b = x y
36 35 eleq1d ⊢ b = y → x b ∈ E ↔ x y ∈ E
37 20 36 rspc2v ⊢ x ∈ A ∧ y ∈ B → ∀ z ∈ A ∀ b ∈ B z b ∈ E → x y ∈ E
38 37 ad2ant2l ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → ∀ z ∈ A ∀ b ∈ B z b ∈ E → x y ∈ E
39 38 impcom ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → x y ∈ E
40 prcom ⊢ y a = a y
41 preq2 ⊢ b = y → a b = a y
42 41 eleq1d ⊢ b = y → a b ∈ E ↔ a y ∈ E
43 10 42 rspc2v ⊢ a ∈ A ∧ y ∈ B → ∀ z ∈ A ∀ b ∈ B z b ∈ E → a y ∈ E
44 43 ad2ant2rl ⊢ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → ∀ z ∈ A ∀ b ∈ B z b ∈ E → a y ∈ E
45 44 impcom ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a y ∈ E
46 40 45 eqeltrid ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → y a ∈ E
47 39 46 jca ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → x y ∈ E ∧ y a ∈ E
48 47 ex ⊢ ∀ z ∈ A ∀ b ∈ B z b ∈ E → a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → x y ∈ E ∧ y a ∈ E
49 8 48 syl ⊢ G ∈ FriendGraph → a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → x y ∈ E ∧ y a ∈ E
50 49 adantr ⊢ G ∈ FriendGraph ∧ a ≠ x → a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → x y ∈ E ∧ y a ∈ E
51 50 impl ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → x y ∈ E ∧ y a ∈ E
52 51 adantr ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ b ≠ y → x y ∈ E ∧ y a ∈ E
53 7 34 52 3jca ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ b ≠ y → a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
54 53 ex ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → b ≠ y → a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
55 54 reximdvva ⊢ G ∈ FriendGraph ∧ a ≠ x ∧ a ∈ A ∧ x ∈ A → ∃ b ∈ B ∃ y ∈ B b ≠ y → ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
56 55 exp31 ⊢ G ∈ FriendGraph → a ≠ x → a ∈ A ∧ x ∈ A → ∃ b ∈ B ∃ y ∈ B b ≠ y → ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
57 56 com24 ⊢ G ∈ FriendGraph → ∃ b ∈ B ∃ y ∈ B b ≠ y → a ∈ A ∧ x ∈ A → a ≠ x → ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
58 57 imp31 ⊢ G ∈ FriendGraph ∧ ∃ b ∈ B ∃ y ∈ B b ≠ y ∧ a ∈ A ∧ x ∈ A → a ≠ x → ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
59 58 reximdvva ⊢ G ∈ FriendGraph ∧ ∃ b ∈ B ∃ y ∈ B b ≠ y → ∃ a ∈ A ∃ x ∈ A a ≠ x → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
60 59 ex ⊢ G ∈ FriendGraph → ∃ b ∈ B ∃ y ∈ B b ≠ y → ∃ a ∈ A ∃ x ∈ A a ≠ x → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
61 60 com13 ⊢ ∃ a ∈ A ∃ x ∈ A a ≠ x → ∃ b ∈ B ∃ y ∈ B b ≠ y → G ∈ FriendGraph → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
62 61 imp ⊢ ∃ a ∈ A ∃ x ∈ A a ≠ x ∧ ∃ b ∈ B ∃ y ∈ B b ≠ y → G ∈ FriendGraph → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
63 1 2 3 4 frgrwopreglem1 ⊢ A ∈ V ∧ B ∈ V
64 hashgt12el ⊢ A ∈ V ∧ 1 < A → ∃ a ∈ A ∃ x ∈ A a ≠ x
65 64 ex ⊢ A ∈ V → 1 < A → ∃ a ∈ A ∃ x ∈ A a ≠ x
66 hashgt12el ⊢ B ∈ V ∧ 1 < B → ∃ b ∈ B ∃ y ∈ B b ≠ y
67 66 ex ⊢ B ∈ V → 1 < B → ∃ b ∈ B ∃ y ∈ B b ≠ y
68 65 67 im2anan9 ⊢ A ∈ V ∧ B ∈ V → 1 < A ∧ 1 < B → ∃ a ∈ A ∃ x ∈ A a ≠ x ∧ ∃ b ∈ B ∃ y ∈ B b ≠ y
69 63 68 ax-mp ⊢ 1 < A ∧ 1 < B → ∃ a ∈ A ∃ x ∈ A a ≠ x ∧ ∃ b ∈ B ∃ y ∈ B b ≠ y
70 62 69 syl11 ⊢ G ∈ FriendGraph → 1 < A ∧ 1 < B → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E
71 70 3impib ⊢ G ∈ FriendGraph ∧ 1 < A ∧ 1 < B → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ E ∧ b x ∈ E ∧ x y ∈ E ∧ y a ∈ E