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